1 /-
2 Copyright (c) 2018 Scott Morrison. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
5 -/
6 import category_theory.whiskering
src └────────────────────────┘
7 import category_theory.yoneda
src └────────────────────┘
8 import category_theory.limits.cones
src └──────────────────────────┘
9 import category_theory.eq_to_hom
src └───────────────────────┘
10
11 open category_theory category_theory.category category_theory.functor opposite
12
13 namespace category_theory.limits
14
15 universes v u u' u'' w -- declare the `v`'s first; see `category_theory.category` for an explanation
16
17 -- See the notes at the top of cones.lean, explaining why we can't allow `J : Prop` here.
18 variables {J K : Type v} [small_category J] [small_category K]
id └──┘ └────────────┘ └────────────┘
src └────────────┘ └────────────┘
typ └──┘ └────────────┘ └────────────┘
doc └────────────┘ └────────────┘
19 variables {C : Type u} [𝒞 : category.{v} C]
id └──┘ └──────┘
src └──────┘
typ └──┘ └──────┘
doc └──────┘
20 include 𝒞
21
22 variables {F : J ⥤ C}
id ┴
src ┴
typ ┴
doc ┴
23
24 /-- A cone `t` on `F` is a limit cone if each cone on `F` admits a unique
25 cone morphism to `t`. -/
26 structure is_limit (t : cone F) :=
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
27 (lift : Π (s : cone F), s.X ⟶ t.X)
id ┴ └──┘ ┴ ┴└┘ ┴ ┴└┘
src ┴ └──┘ └┘ ┴ └┘
typ ┴ └──┘ ┴ ┴└┘ ┴ ┴└┘
doc └──┘
28 (fac' : ∀ (s : cone F) (j : J), lift s ≫ t.π.app j = s.π.app j . obviously)
id ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴└┘└──┘ ┴ ┴
src ┴ └──┘ └──┘ ┴ └┘└──┘ ┴ └┘└──┘
typ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴└┘└──┘ ┴ ┴
doc ┴ └──┘
29 (uniq' : ∀ (s : cone F) (m : s.X ⟶ t.X) (w : ∀ j : J, m ≫ t.π.app j = s.π.app j),
id ┴ └──┘ ┴ ┴└┘ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴└┘└──┘ ┴
src ┴ └──┘ └┘ ┴ └┘ ┴ └┘└──┘ ┴ └┘└──┘
typ ┴ └──┘ ┴ ┴└┘ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴└┘└──┘ ┴
doc ┴ └──┘
30 m = lift s . obviously)
id ┴ ┴ └──┘ ┴ ┴
src ┴ └──┘
typ ┴ ┴ └──┘ ┴ ┴
31
32 restate_axiom is_limit.fac'
33 attribute [simp] is_limit.fac
id └──────────┘
typ └──────────┘
doc └──┘
34 restate_axiom is_limit.uniq'
35
36 namespace is_limit
37
38 instance subsingleton {t : cone F} : subsingleton (is_limit t) :=
id └──┘ ┴ └──────────┘ └──────┘ ┴
src └──┘ └──────────┘ └──────┘
typ └──┘ ┴ └──────────┘ └──────┘ ┴
doc └──┘ └──────┘
39 ⟨by intros P Q; cases P; cases Q; congr; ext; solve_by_elim⟩
id ┴ ┴
src └────────┘ └────┘ └────┘ └───┘ └─┘ └───────────┘
typ └────────┘ └────┘┴ └────┘┴ └───┘ └─┘ └───────────┘
doc └────────┘ └────┘ └────┘ └─┘ └───────────┘
txt └────────┘ └────┘ └────┘ └───┘ └─┘ └───────────┘
par └────────┘ └────┘ └────┘ └───┘ └─┘ └───────────┘
pid └──┘ ┴ ┴
st └──────────────────────────────────────────────────────┘
40
41 /- Repackaging the definition in terms of cone morphisms. -/
42
43 def lift_cone_morphism {t : cone F} (h : is_limit t) (s : cone F) : s ⟶ t :=
id └──┘ ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘ └──────┘ └──┘ ┴
typ └──┘ ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘ └──────┘ └──┘
44 { hom := h.lift s }
id ┴ ┴└───┘ ┴
src ┴ └───┘
typ ┴ ┴└───┘ ┴
doc ┴
45
46 lemma uniq_cone_morphism {s t : cone F} (h : is_limit t) {f f' : s ⟶ t} :
id └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └──────┘ ┴
typ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──┘ └──────┘
47 f = f' :=
id ┴ ┴ └┘
src ┴
typ ┴ ┴ └┘
48 have ∀ {g : s ⟶ t}, g = h.lift_cone_morphism s, by intro g; ext; exact h.uniq _ _ g.w,
id ┴ ┴ ┴ ┴ ┴ ┴└─────────────────┘ ┴ └────┘ └─┘
src ┴ ┴ └─────────────────┘ └─────┘ └─┘ └────┘ └───┘└─┘
typ ┴ ┴ ┴ ┴ ┴ ┴└─────────────────┘ ┴ └─────┘ └─┘ └────┘└────┘└───┘└─┘
doc └─────┘ └─┘ └────┘ └───┘
txt └─────┘ └─┘ └────┘ └───┘
par └─────┘ └─┘ └────┘ └───┘
pid └┘ ┴ └───┘
st └─────────────────────────────────┘
49 this.trans this.symm
id └──┘└────┘ └──┘└───┘
src └────┘ └───┘
typ └──┘└────┘ └──┘└───┘
50
51 def mk_cone_morphism {t : cone F}
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
st └──┘└──────────┘
52 (lift : Π (s : cone F), s ⟶ t)
id └──┘ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴
doc └──┘
53 (uniq' : ∀ (s : cone F) (m : s ⟶ t), m = lift s) : is_limit t :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──────┘ ┴
src └──┘ ┴ ┴ └──┘ └──────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──────┘ ┴
doc └──┘ └──────┘
54 { lift := λ s, (lift s).hom,
id ┴ ┴ └──┘ ┴ └─┘
src ┴ └──┘ └─┘
typ ┴ ┴ └──┘ ┴ └─┘
doc ┴
55 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
56 have cone_morphism.mk m w = lift s, by apply uniq',
id └──────────────┘ ┴ ┴ ┴ └──┘ ┴
src └──────────────┘ ┴ └──┘ └────┘
typ └──────────────┘ ┴ ┴ ┴ └──┘ ┴ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st └──────────┘
57 congr_arg cone_morphism.hom this }
id └───────┘ └───────────────┘ └──┘
src └───────┘ └───────────────┘
typ └───────┘ └───────────────┘ └──┘
58
59 /-- Limit cones on `F` are unique up to isomorphism. -/
60 def unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s ≅ t :=
id └──┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └──────┘ └──────┘ ┴
typ └──┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──┘ └──────┘ └──────┘
61 { hom := Q.lift_cone_morphism s,
id ┴└─────────────────┘ ┴
src └─────────────────┘
typ ┴└─────────────────┘ ┴
62 inv := P.lift_cone_morphism t,
id ┴└─────────────────┘ ┴
src └─────────────────┘
typ ┴└─────────────────┘ ┴
63 hom_inv_id' := P.uniq_cone_morphism,
id ┴└─────────────────┘
src └─────────────────┘
typ ┴└─────────────────┘
64 inv_hom_id' := Q.uniq_cone_morphism }
id ┴└─────────────────┘
src └─────────────────┘
typ ┴└─────────────────┘
65
66 def of_iso_limit {r t : cone F} (P : is_limit r) (i : r ≅ t) : is_limit t :=
id └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └──┘ └──────┘ ┴ └──────┘
typ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──┘ └──────┘ └──────┘
67 is_limit.mk_cone_morphism
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
68 (λ s, P.lift_cone_morphism s ≫ i.hom)
id ┴ ┴└─────────────────┘ ┴ ┴ ┴└──┘
src └─────────────────┘ ┴ └──┘
typ ┴ ┴└─────────────────┘ ┴ ┴ ┴└──┘
69 (λ s m, by rw ←i.comp_inv_eq; apply P.uniq_cone_morphism)
id ┴ ┴
src └──┘ └────┘
typ ┴ ┴ └──┘└───────────┘ └────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid └┘ ┴
st └────────────────────────────────────────────┘
70
71 variables {t : cone F}
id └──┘
src └──┘
typ └──┘
doc └──┘
72
73 lemma hom_lift (h : is_limit t) {W : C} (m : W ⟶ t.X) :
id └──────┘ ┴ ┴ ┴ ┴ ┴└┘
src └──────┘ ┴ └┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴└┘
doc └──────┘
74 m = h.lift { X := W, π := { app := λ b, m ≫ t.π.app b } } :=
id ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴
src ┴ └───┘ ┴ ┴ └┘└──┘
typ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴
doc ┴
75 h.uniq { X := W, π := { app := λ b, m ≫ t.π.app b } } m (λ b, rfl)
id ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴ └─┘
src ┴ ┴ └┘└──┘ └─┘
typ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴ └─┘
doc ┴
76
77 /-- Two morphisms into a limit are equal if their compositions with
78 each cone morphism are equal. -/
79 lemma hom_ext (h : is_limit t) {W : C} {f f' : W ⟶ t.X}
id └──────┘ ┴ ┴ ┴ ┴ ┴└┘
src └──────┘ ┴ └┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴└┘
doc └──────┘
80 (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) : f = f' :=
id ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ └┘ ┴ ┴└┘└──┘ ┴ ┴ ┴ └┘
src ┴ └┘└──┘ ┴ ┴ └┘└──┘ ┴
typ ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ └┘ ┴ ┴└┘└──┘ ┴ ┴ ┴ └┘
81 by rw [h.hom_lift f, h.hom_lift f']; congr; exact funext w
id └────────┘ ┴ └────────┘ └┘ └────┘ ┴
src └──┘└────────┘┴ └┘└────────┘┴ ┴ └───┘ └────┘└────┘┴ └
typ └──┘└────────┘┴┴└┘└────────┘┴└┘┴ └───┘ └────┘└────┘┴┴└
doc └──┘ ┴ └┘ ┴ ┴ └────┘ ┴ └
txt └──┘ ┴ └┘ ┴ ┴ └───┘ └────┘ ┴ └
par └──┘ ┴ └┘ ┴ ┴ └───┘ └────┘ ┴ └
pid └┘ ┴ └┘ ┴ ┴ ┴ ┴ └
st └───────────────┘└─────────────┘┴└───────────────────────
82
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
83 /-- The universal property of a limit cone: a map `W ⟶ X` is the same as
84 a cone on `F` with vertex `W`. -/
85 def hom_iso (h : is_limit t) (W : C) : (W ⟶ t.X) ≅ ((const J).obj W ⟶ F) :=
id └──────┘ ┴ ┴ ┴ ┴ ┴└┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴
src └──────┘ ┴ └┘ ┴ └───┘ └─┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴└┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴
doc └──────┘
86 { hom := λ f, (t.extend f).π,
id ┴ ┴ ┴└─────┘ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ ┴└─────┘ ┴ ┴
doc ┴ └─────┘
87 inv := λ π, h.lift { X := W, π := π },
id ┴ ┴└───┘ ┴ ┴
src └───┘
typ ┴ ┴└───┘ ┴ ┴
88 hom_inv_id' := by ext f; apply h.hom_ext; intro j; simp; dsimp; refl }
src └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
typ └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
doc └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
txt └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
par └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
pid └┘ ┴ └┘ ┴
st └──────────────────────────────────────────────────┘
89
90 @[simp] lemma hom_iso_hom (h : is_limit t) {W : C} (f : W ⟶ t.X) :
id └──────┘ ┴ ┴ ┴ ┴ ┴└┘
src └──────┘ ┴ └┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴└┘
doc └──┘ └──────┘
91 (is_limit.hom_iso h W).hom f = (t.extend f).π := rfl
id └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴└─────┘ ┴ ┴ └─┘
src └──────────────┘ └─┘ ┴ └─────┘ ┴ └─┘
typ └──────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴└─────┘ ┴ ┴ └─┘
doc └──────────────┘ └─────┘
92
93 /-- The limit of `F` represents the functor taking `W` to
94 the set of cones on `F` with vertex `W`. -/
95 def nat_iso (h : is_limit t) : yoneda.obj t.X ≅ F.cones :=
id └──────┘ ┴ └────┘└──┘ ┴└┘ ┴ ┴└────┘
src └──────┘ └────┘└──┘ └┘ ┴ └────┘
typ └──────┘ ┴ └────┘└──┘ ┴└┘ ┴ ┴└────┘
doc └──────┘ └────┘
96 nat_iso.of_components (λ W, is_limit.hom_iso h (unop W)) (by tidy).
id └───────────────────┘ ┴ └──────────────┘ ┴ └──┘ ┴
src └───────────────────┘ └──────────────┘ └──┘ └──┘
typ └───────────────────┘ ┴ └──────────────┘ ┴ └──┘ ┴ └──┘
doc └──────────────┘ └──┘
txt └──┘
par └──┘
st └───┘
97
98 def hom_iso' (h : is_limit t) (W : C) :
id └──────┘ ┴ ┴
src └──────┘
typ └──────┘ ┴ ┴
doc └──────┘
99 ((W ⟶ t.X) : Type v) ≅ { p : Π j, W ⟶ F.obj j // ∀ {j j'} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
id ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ └┘
src ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ └┘
100 h.hom_iso W ≪≫
id ┴└──────┘ ┴ └┘
src └──────┘ └┘
typ ┴└──────┘ ┴ └┘
doc └──────┘
101 { hom := λ π,
id ┴ ┴
src ┴
typ ┴ ┴
doc ┴
102 ⟨λ j, π.app j, λ j j' f,
id ┴ ┴└──┘ ┴ ┴ └┘ ┴
src └──┘
typ ┴ ┴└──┘ ┴ ┴ └┘ ┴
103 by convert ←(π.naturality f).symm; apply id_comp⟩,
id └──────────┘ ┴ └─────┘
src └───────┘ └──────────┘┴ └────┘ └────┘└─────┘
typ └───────┘ └──────────┘┴┴└────┘ └────┘└─────┘
doc └───────┘ ┴ └────┘ └────┘
txt └───────┘ ┴ └────┘ └────┘
par └───────┘ ┴ └────┘ └────┘
pid └┘ ┴ └───┘┴ ┴
st └────────────────────────────────────────────┘
104 inv := λ p,
id ┴
typ ┴
105 { app := λ j, p.1 j,
id ┴ ┴┴ ┴
src ┴
typ ┴ ┴┴ ┴
st ┴
106 naturality' := λ j j' f, begin dsimp, rw [id_comp], exact (p.2 f).symm end } }
id ┴ └┘ ┴ └─────┘ ┴ ┴
src └───┘ └──┘└─────┘┴ └────┘ └─┘ └─────┘
typ ┴ └┘ ┴ └───┘ └──┘└─────┘┴ └────┘ ┴└─┘┴└─────┘
doc └───┘ └──┘ ┴ └────┘ └─┘ └─────┘
txt └───┘ └──┘ ┴ └────┘ └─┘ └─────┘
par └───┘ └──┘ ┴ └────┘ └─┘ └─────┘
pid └┘ ┴ ┴ └─┘ └───┘└┘
st └─────────┘└───────────┘└────────────────────┘└─┘
107
108 /-- If G : C → D is a faithful functor which sends t to a limit cone,
109 then it suffices to check that the induced maps for the image of t
110 can be lifted to maps of C. -/
111 def of_faithful {t : cone F} {D : Type u'} [category.{v} D] (G : C ⥤ D) [faithful G]
id └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └──┘ └──────┘ ┴ └──────┘
typ └──┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──┘ └──────┘ ┴ └──────┘
112 (ht : is_limit (G.map_cone t)) (lift : Π (s : cone F), s.X ⟶ t.X)
id └──────┘ ┴└───────┘ ┴ └──┘ ┴ ┴└┘ ┴ ┴└┘
src └──────┘ └───────┘ └──┘ └┘ ┴ └┘
typ └──────┘ ┴└───────┘ ┴ └──┘ ┴ ┴└┘ ┴ ┴└┘
doc └──────┘ └───────┘ └──┘
113 (h : ∀ s, G.map (lift s) = ht.lift (G.map_cone s)) : is_limit t :=
id ┴ ┴└──┘ └──┘ ┴ ┴ └┘└───┘ ┴└───────┘ ┴ └──────┘ ┴
src └──┘ └──┘ ┴ └───┘ └───────┘ └──────┘
typ ┴ ┴└──┘ └──┘ ┴ ┴ └┘└───┘ ┴└───────┘ ┴ └──────┘ ┴
doc └───────┘ └──────┘
114 { lift := lift,
id └──┘
src └──┘
typ └──┘
115 fac' := λ s j, by apply G.injectivity; rw [G.map_comp, h]; apply ht.fac,
id ┴ ┴ ┴
src └────┘ └──┘ └┘ ┴ └────┘
typ ┴ ┴ └────┘ └──┘└────────┘└┘┴┴ └────┘
doc └────┘ └──┘ └┘ ┴ └────┘
txt └────┘ └──┘ └┘ ┴ └────┘
par └────┘ └──┘ └┘ ┴ └────┘
pid ┴ └┘ └┘ ┴ ┴
st └────────────────────────┘└────────┘└─┘┴└────────────┘
116 uniq' := λ s m w, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └─────
117 apply G.injectivity, rw h,
id ┴
src └────┘ └─┘
typ └────┘ └─┘┴
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ ┴
st ──────────────────────┘└────┘└─
118 refine ht.uniq (G.map_cone s) _ (λ j, _),
id └─────┘ └────────┘ ┴
src └─────┘ ┴ └────────┘┴ └──┘ └────┘
typ └─────┘└─────┘┴ └────────┘┴┴└──┘ └────┘
doc └─────┘ ┴ └────────┘┴ └──┘ └────┘
txt └─────┘ ┴ ┴ └──┘ └────┘
par └─────┘ ┴ ┴ └──┘ └────┘
pid ┴ ┴ ┴ └──┘ └────┘
st ───────────────────────────────────────────┘└─
119 convert ←congr_arg (λ f, G.map f) (w j),
id └───────┘ └───┘ ┴ ┴
src └───────┘└───────┘┴ └──┘└───┘┴ └┘ ┴ ┴
typ └───────┘└───────┘┴ └──┘└───┘┴ └┘ ┴┴┴┴
doc └───────┘ ┴ └──┘ ┴ └┘ ┴ ┴
txt └───────┘ ┴ └──┘ ┴ └┘ ┴ ┴
par └───────┘ ┴ └──┘ ┴ └┘ ┴ ┴
pid └┘ ┴ └──┘ ┴ └┘ ┴ ┴
st ──────────────────────────────────────────┘└─
120 apply G.map_comp
src └────┘ └
typ └────┘ └
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────
121 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
122
123 def iso_unique_cone_morphism {t : cone F} :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
124 is_limit t ≅ Π s, unique (s ⟶ t) :=
id └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └──────┘ ┴ └────┘ ┴
typ └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └──────┘
125 { hom := λ h s,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
126 { default := h.lift_cone_morphism s,
id ┴└─────────────────┘ ┴
src └─────────────────┘
typ ┴└─────────────────┘ ┴
127 uniq := λ _, h.uniq_cone_morphism },
id ┴ ┴└─────────────────┘
src └─────────────────┘
typ ┴ ┴└─────────────────┘
128 inv := λ h,
id ┴
typ ┴
129 { lift := λ s, (h s).default.hom,
id ┴ ┴ ┴ ┴ └─────┘ └─┘
src ┴ └─────┘ └─┘
typ ┴ ┴ ┴ ┴ └─────┘ └─┘
doc ┴
130 uniq' := λ s f w, congr_arg cone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
id ┴ ┴ ┴ └───────┘ └───────────────┘ ┴ ┴ └──┘ ┴ ┴
src └───────┘ └───────────────┘ └──┘
typ ┴ ┴ ┴ └───────┘ └───────────────┘ ┴ ┴ └──┘ ┴ ┴
131
132 namespace of_nat_iso
133 variables {X : C} (h : yoneda.obj X ≅ F.cones)
id └────┘└──┘ ┴ └────┘
src └────┘└──┘ ┴ └────┘
typ └────┘└──┘ ┴ └────┘
doc └────┘
134
135 /-- If `F.cones` is represented by `X`, each morphism `f : Y ⟶ X` gives a cone with cone point `Y`. -/
136 def cone_of_hom {Y : C} (f : Y ⟶ X) : cone F :=
id ┴ ┴ ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘
137 { X := Y, π := h.hom.app (op Y) f }
id ┴ ┴└──┘└──┘ └┘ ┴ ┴
src └──┘└──┘ └┘
typ ┴ ┴└──┘└──┘ └┘ ┴ ┴
138
139 /-- If `F.cones` is represented by `X`, each cone `s` gives a morphism `s.X ⟶ X`. -/
140 def hom_of_cone (s : cone F) : s.X ⟶ X := h.inv.app (op s.X) s.π
id └──┘ ┴ ┴└┘ ┴ ┴ ┴└──┘└──┘ └┘ ┴└┘ ┴└┘
src └──┘ └┘ ┴ └──┘└──┘ └┘ └┘ └┘
typ └──┘ ┴ ┴└┘ ┴ ┴ ┴└──┘└──┘ └┘ ┴└┘ ┴└┘
doc └──┘
141
142 @[simp] lemma cone_of_hom_of_cone (s : cone F) : cone_of_hom h (hom_of_cone h s) = s :=
id └──┘ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴
src └──┘ └─────────┘ └─────────┘ ┴
typ └──┘ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘ └─────────┘ └─────────┘
143 begin
st └─────
144 dsimp [cone_of_hom, hom_of_cone], cases s, congr, dsimp,
id └─────────┘ └─────────┘ ┴
src └─────┘└─────────┘└┘└─────────┘┴ └────┘ └───┘ └───┘
typ └─────┘└─────────┘└┘└─────────┘┴ └────┘┴ └───┘ └───┘
doc └─────┘└─────────┘└┘└─────────┘┴ └────┘ └───┘
txt └─────┘ └┘ ┴ └────┘ └───┘ └───┘
par └─────┘ └┘ ┴ └────┘ └───┘ └───┘
pid ┴┴ └┘ ┴ ┴
st ─────────────────────────────────┘└───────┘└─────┘└─────┘└─
145 exact congr_fun (congr_fun (congr_arg nat_trans.app h.inv_hom_id) (op s_X)) s_π,
id └───────┘ └───────┘ └───────────┘ └──────────┘ └┘ └─┘ └─┘
src └────┘ ┴ └───────┘┴ └───────┘┴└───────────┘┴└──────────┘└┘ └┘┴ └─┘
typ └────┘ ┴ └───────┘┴ └───────┘┴└───────────┘┴└──────────┘└┘ └┘┴└─┘└─┘└─┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
par └────┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────────────┘└─
146 end
st ──┘
147
148 @[simp] lemma hom_of_cone_of_hom {Y : C} (f : Y ⟶ X) : hom_of_cone h (cone_of_hom h f) = f :=
id ┴ ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴
src ┴ └─────────┘ └─────────┘ ┴
typ ┴ ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴
doc └──┘ └─────────┘ └─────────┘
149 congr_fun (congr_fun (congr_arg nat_trans.app h.hom_inv_id) (op Y)) f
id └───────┘ └───────┘ └───────┘ └───────────┘ ┴└─────────┘ └┘ ┴ ┴
src └───────┘ └───────┘ └───────┘ └───────────┘ └─────────┘ └┘
typ └───────┘ └───────┘ └───────┘ └───────────┘ ┴└─────────┘ └┘ ┴ ┴
150
151 /-- If `F.cones` is represented by `X`, the cone corresponding to the identity morphism on `X`
152 will be a limit cone. -/
153 def limit_cone : cone F :=
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
154 cone_of_hom h (𝟙 X)
id └─────────┘ ┴ ┴ ┴
src └─────────┘ ┴
typ └─────────┘ ┴ ┴ ┴
doc └─────────┘
155
156 /-- If `F.cones` is represented by `X`, the cone corresponding to a morphism `f : Y ⟶ X` is
157 the limit cone extended by `f`. -/
158 lemma cone_of_hom_fac {Y : C} (f : Y ⟶ X) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
159 cone_of_hom h f = (limit_cone h).extend f :=
id └─────────┘ ┴ ┴ ┴ └────────┘ ┴ └────┘ ┴
src └─────────┘ ┴ └────────┘ └────┘
typ └─────────┘ ┴ ┴ ┴ └────────┘ ┴ └────┘ ┴
doc └─────────┘ └────────┘ └────┘
160 begin
st └─────
161 dsimp [cone_of_hom, limit_cone, cone.extend],
id └─────────┘ └────────┘ └─────────┘
src └─────┘└─────────┘└┘└────────┘└┘└─────────┘┴
typ └─────┘└─────────┘└┘└────────┘└┘└─────────┘┴
doc └─────┘└─────────┘└┘└────────┘└┘└─────────┘┴
txt └─────┘ └┘ └┘ ┴
par └─────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ─────────────────────────────────────────────┘└─
162 congr,
src └───┘
typ └───┘
txt └───┘
par └───┘
st ──────┘└─
163 ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
164 have t := congr_fun (h.hom.naturality f.op) (𝟙 X),
id └───────┘ └──────────────┘ └──┘ ┴ ┴
src └────────┘└───────┘┴ └──────────────┘┴└──┘└┘ ┴┴ ┴
typ └────────┘└───────┘┴ └──────────────┘┴└──┘└┘ ┴┴┴┴
doc └────────┘ ┴ ┴ └┘ ┴ ┴
txt └────────┘ ┴ ┴ └┘ ┴ ┴
par └────────┘ ┴ ┴ └┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ └┘ ┴ ┴
st ──────────────────────────────────────────────────┘└─
165 dsimp at t,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└──┘
st ───────────┘└─
166 simp only [comp_id] at t,
id └─────┘
src └─────────┘└─────┘└────┘
typ └─────────┘└─────┘└────┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid ┴└──┘└┘ ┴┴└──┘
st ─────────────────────────┘└─
167 rw congr_fun (congr_arg nat_trans.app t) j,
id └───────┘ └───────┘ └───────────┘ ┴ ┴
src └─┘└───────┘┴ └───────┘┴└───────────┘┴ └┘
typ └─┘└───────┘┴ └───────┘┴└───────────┘┴┴└┘┴
doc └─┘ ┴ ┴ ┴ └┘
txt └─┘ ┴ ┴ ┴ └┘
par └─┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────┘└─
168 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└─
169 end
st ──┘
170
171 /-- If `F.cones` is represented by `X`, any cone is the extension of the limit cone by the
172 corresponding morphism. -/
173 lemma cone_fac (s : cone F) : (limit_cone h).extend (hom_of_cone h s) = s :=
id └──┘ ┴ └────────┘ ┴ └────┘ └─────────┘ ┴ ┴ ┴ ┴
src └──┘ └────────┘ └────┘ └─────────┘ ┴
typ └──┘ ┴ └────────┘ ┴ └────┘ └─────────┘ ┴ ┴ ┴ ┴
doc └──┘ └────────┘ └────┘ └─────────┘
174 begin
st └─────
175 rw ←cone_of_hom_of_cone h s,
id └─────────────────┘ ┴ ┴
src └──┘└─────────────────┘┴ ┴
typ └──┘└─────────────────┘┴┴┴┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ────────────────────────────┘└─
176 conv_lhs { simp only [hom_of_cone_of_hom] },
id └────────────────┘
src └─────────┘└─────────┘└────────────────┘└┘┴
typ └─────────┘└─────────┘└────────────────┘└┘┴
txt └─────────┘└─────────┘ └┘┴
par └─────────┘└─────────┘ └┘┴
pid ┴└───────────┘ └─┘
st ───────────┘└──────────────────────────────┘└┘└
177 apply (cone_of_hom_fac _ _).symm,
id └─────────────┘
src └────┘ └─────────────┘└────────┘
typ └────┘ └─────────────┘└────────┘
doc └────┘ └─────────────┘└────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └───────┘┴
st ─────────────────────────────────┘└─
178 end
st ──┘
179
180 end of_nat_iso
181
182 section
183 open of_nat_iso
184
185 /--
186 If `F.cones` is representable, then the cone corresponding to the identity morphism on
187 the representing object is a limit cone.
188 -/
189 def of_nat_iso {X : C} (h : yoneda.obj X ≅ F.cones) :
id ┴ └────┘└──┘ ┴ ┴ ┴└────┘
src └────┘└──┘ ┴ └────┘
typ ┴ └────┘└──┘ ┴ ┴ ┴└────┘
doc └────┘
190 is_limit (limit_cone h) :=
id └──────┘ └────────┘ ┴
src └──────┘ └────────┘
typ └──────┘ └────────┘ ┴
doc └──────┘ └────────┘
191 { lift := λ s, hom_of_cone h s,
id ┴ └─────────┘ ┴ ┴
src └─────────┘
typ ┴ └─────────┘ ┴ ┴
doc └─────────┘
192 fac' := λ s j,
id ┴ ┴
typ ┴ ┴
193 begin
st └─────
194 have h := cone_fac h s,
id └──────┘ ┴ ┴
src └────────┘└──────┘┴ ┴
typ └────────┘└──────┘┴┴┴┴
doc └────────┘└──────┘┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ─────────────────────────┘└─
195 cases s,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────┘└─
196 injection h with h₁ h₂,
id ┴
src └────────┘ └─────────┘
typ └────────┘┴└─────────┘
doc └────────┘ └─────────┘
txt └────────┘ └─────────┘
par └────────┘ └─────────┘
pid ┴ └─────────┘
st ─────────────────────────┘└─
197 simp only [heq_iff_eq] at h₂,
id └────────┘
src └─────────┘└────────┘└─────┘
typ └─────────┘└────────┘└─────┘
doc └─────────┘ └─────┘
txt └─────────┘ └─────┘
par └─────────┘ └─────┘
pid ┴└──┘└┘ ┴┴└───┘
st ───────────────────────────────┘└─
198 conv_rhs { rw ← h₂ }, refl,
id └┘
src └─────────┘└───┘ ┴┴ └──┘
typ └─────────┘└───┘└┘┴┴ └──┘
doc └──┘
txt └─────────┘└───┘ ┴┴ └──┘
par └─────────┘└───┘ ┴┴ └──┘
pid ┴└─────┘ └┘
st ─────────────┘└───────┘└┘└───┘└─
199 end,
st ────┘
200 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
201 begin
st └─────
202 rw ←hom_of_cone_of_hom h m,
id └────────────────┘ ┴ ┴
src └──┘└────────────────┘┴ ┴
typ └──┘└────────────────┘┴┴┴┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ─────────────────────────────┘└─
203 congr,
src └───┘
typ └───┘
txt └───┘
par └───┘
st ────────┘└─
204 rw cone_of_hom_fac,
id └─────────────┘
src └─┘└─────────────┘
typ └─┘└─────────────┘
doc └─┘└─────────────┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────┘└─
205 dsimp, cases s, congr,
id ┴
src └───┘ └────┘ └───┘
typ └───┘ └────┘┴ └───┘
doc └───┘ └────┘
txt └───┘ └────┘ └───┘
par └───┘ └────┘ └───┘
pid ┴
st ────────┘└───────┘└─────┘└─
206 ext j, exact w j,
id ┴ ┴
src └───┘ └────┘ ┴
typ └───┘ └────┘┴┴┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid └┘ ┴ ┴
st ────────┘└─────────┘└─
207 end }
st ────┘
208 end
209
210 end is_limit
211
212 /-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
213 cocone morphism from `t`. -/
214 structure is_colimit (t : cocone F) :=
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
215 (desc : Π (s : cocone F), t.X ⟶ s.X)
id ┴ └────┘ ┴ ┴└┘ ┴ ┴└┘
src └────┘ └┘ ┴ └┘
typ ┴ └────┘ ┴ ┴└┘ ┴ ┴└┘
doc └────┘
216 (fac' : ∀ (s : cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j . obviously)
id ┴ └────┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ └──┘ ┴ ┴ ┴└┘└──┘ ┴ ┴
src ┴ └────┘ └┘└──┘ ┴ ┴ └┘└──┘
typ ┴ └────┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ └──┘ ┴ ┴ ┴└┘└──┘ ┴ ┴
doc ┴ └────┘
217 (uniq' : ∀ (s : cocone F) (m : t.X ⟶ s.X) (w : ∀ j : J, t.ι.app j ≫ m = s.ι.app j),
id ┴ └────┘ ┴ ┴└┘ ┴ ┴└┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴
src ┴ └────┘ └┘ ┴ └┘ └┘└──┘ ┴ ┴ └┘└──┘
typ ┴ └────┘ ┴ ┴└┘ ┴ ┴└┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴
doc ┴ └────┘
218 m = desc s . obviously)
id ┴ ┴ └──┘ ┴ ┴
src ┴
typ ┴ ┴ └──┘ ┴ ┴
219
220 restate_axiom is_colimit.fac'
221 attribute [simp] is_colimit.fac
id └────────────┘
typ └────────────┘
doc └──┘
222 restate_axiom is_colimit.uniq'
223
224 namespace is_colimit
225
226 instance subsingleton {t : cocone F} : subsingleton (is_colimit t) :=
id └────┘ ┴ └──────────┘ └────────┘ ┴
src └────┘ └──────────┘ └────────┘
typ └────┘ ┴ └──────────┘ └────────┘ ┴
doc └────┘ └────────┘
227 ⟨by intros P Q; cases P; cases Q; congr; ext; solve_by_elim⟩
id ┴ ┴
src └────────┘ └────┘ └────┘ └───┘ └─┘ └───────────┘
typ └────────┘ └────┘┴ └────┘┴ └───┘ └─┘ └───────────┘
doc └────────┘ └────┘ └────┘ └─┘ └───────────┘
txt └────────┘ └────┘ └────┘ └───┘ └─┘ └───────────┘
par └────────┘ └────┘ └────┘ └───┘ └─┘ └───────────┘
pid └──┘ ┴ ┴
st └──────────────────────────────────────────────────────┘
228
229 /- Repackaging the definition in terms of cone morphisms. -/
230
231 def desc_cocone_morphism {t : cocone F} (h : is_colimit t) (s : cocone F) : t ⟶ s :=
id └────┘ ┴ └────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘ └────────┘ └────┘ ┴
typ └────┘ ┴ └────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └────┘ └────────┘ └────┘
232 { hom := h.desc s }
id ┴ ┴└───┘ ┴
src ┴ └───┘
typ ┴ ┴└───┘ ┴
doc ┴
233
234 lemma uniq_cocone_morphism {s t : cocone F} (h : is_colimit t) {f f' : t ⟶ s} :
id └────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src └────┘ └────────┘ ┴
typ └────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────┘ └────────┘
235 f = f' :=
id ┴ ┴ └┘
src ┴
typ ┴ ┴ └┘
236 have ∀ {g : t ⟶ s}, g = h.desc_cocone_morphism s, by intro g; ext; exact h.uniq _ _ g.w,
id ┴ ┴ ┴ ┴ ┴ ┴└───────────────────┘ ┴ └────┘ └─┘
src ┴ ┴ └───────────────────┘ └─────┘ └─┘ └────┘ └───┘└─┘
typ ┴ ┴ ┴ ┴ ┴ ┴└───────────────────┘ ┴ └─────┘ └─┘ └────┘└────┘└───┘└─┘
doc └─────┘ └─┘ └────┘ └───┘
txt └─────┘ └─┘ └────┘ └───┘
par └─────┘ └─┘ └────┘ └───┘
pid └┘ ┴ └───┘
st └─────────────────────────────────┘
237 this.trans this.symm
id └──┘└────┘ └──┘└───┘
src └────┘ └───┘
typ └──┘└────┘ └──┘└───┘
238
239 def mk_cocone_morphism {t : cocone F}
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
240 (desc : Π (s : cocone F), t ⟶ s)
id └────┘ ┴ ┴ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴ ┴ ┴
doc └────┘
241 (uniq' : ∀ (s : cocone F) (m : t ⟶ s), m = desc s) : is_colimit t :=
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────────┘ ┴
src └────┘ ┴ ┴ └────────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └────────┘ ┴
doc └────┘ └────────┘
242 { desc := λ s, (desc s).hom,
id ┴ ┴ └──┘ ┴ └─┘
src ┴ └─┘
typ ┴ ┴ └──┘ ┴ └─┘
doc ┴
243 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
244 have cocone_morphism.mk m w = desc s, by apply uniq',
id └────────────────┘ ┴ ┴ ┴ └──┘ ┴
src └────────────────┘ ┴ └────┘
typ └────────────────┘ ┴ ┴ ┴ └──┘ ┴ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st └──────────┘
245 congr_arg cocone_morphism.hom this }
id └───────┘ └─────────────────┘ └──┘
src └───────┘ └─────────────────┘
typ └───────┘ └─────────────────┘ └──┘
246
247 /-- Limit cones on `F` are unique up to isomorphism. -/
248 def unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s ≅ t :=
id └────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
src └────┘ └────────┘ └────────┘ ┴
typ └────┘ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └────┘ └────────┘ └────────┘
249 { hom := P.desc_cocone_morphism t,
id ┴└───────────────────┘ ┴
src └───────────────────┘
typ ┴└───────────────────┘ ┴
250 inv := Q.desc_cocone_morphism s,
id ┴└───────────────────┘ ┴
src └───────────────────┘
typ ┴└───────────────────┘ ┴
251 hom_inv_id' := P.uniq_cocone_morphism,
id ┴└───────────────────┘
src └───────────────────┘
typ ┴└───────────────────┘
252 inv_hom_id' := Q.uniq_cocone_morphism }
id ┴└───────────────────┘
src └───────────────────┘
typ ┴└───────────────────┘
253
254 def of_iso_colimit {r t : cocone F} (P : is_colimit r) (i : r ≅ t) : is_colimit t :=
id └────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
src └────┘ └────────┘ ┴ └────────┘
typ └────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └────┘ └────────┘ └────────┘
255 is_colimit.mk_cocone_morphism
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
256 (λ s, i.inv ≫ P.desc_cocone_morphism s)
id ┴ ┴└──┘ ┴ ┴└───────────────────┘ ┴
src └──┘ ┴ └───────────────────┘
typ ┴ ┴└──┘ ┴ ┴└───────────────────┘ ┴
257 (λ s m, by rw i.eq_inv_comp; apply P.uniq_cocone_morphism)
id ┴ ┴
src └─┘ └────┘
typ ┴ ┴ └─┘└───────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └─────────────────────────────────────────────┘
258
259 variables {t : cocone F}
id └────┘
src └────┘
typ └────┘
doc └────┘
260
261 lemma hom_desc (h : is_colimit t) {W : C} (m : t.X ⟶ W) :
id └────────┘ ┴ ┴ ┴└┘ ┴ ┴
src └────────┘ └┘ ┴
typ └────────┘ ┴ ┴ ┴└┘ ┴ ┴
doc └────────┘
262 m = h.desc { X := W, ι := { app := λ b, t.ι.app b ≫ m,
id ┴ ┴ ┴└───┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴
src ┴ └───┘ └┘└──┘ ┴
typ ┴ ┴ ┴└───┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴
263 naturality' := by intros; erw [←assoc, t.ι.naturality, comp_id, comp_id] } } :=
id └───┘ └─────┘ └─────┘
src └────┘ └────┘└───┘└┘ └┘└─────┘└┘└─────┘└┘
typ └────┘ └────┘└───┘└┘└────────────┘└┘└─────┘└┘└─────┘└┘
doc └────┘ └────┘ └┘ └┘ └┘ └┘
txt └────┘ └────┘ └┘ └┘ └┘ └┘
par └────┘ └────┘ └┘ └┘ └┘ └┘
pid └─┘ └┘ └┘ └┘ ┴┴
st └────────────┘└────┘└──────────────┘└───────┘└───────┘┴┴
264 h.uniq { X := W, ι := { app := λ b, t.ι.app b ≫ m, naturality' := _ } } m (λ b, rfl)
id ┴└───┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └┘└──┘ ┴ └─┘
typ ┴└───┘ ┴ ┴ ┴└┘└──┘ ┴ ┴ ┴ ┴ ┴ └─┘
265
266 /-- Two morphisms out of a colimit are equal if their compositions with
267 each cocone morphism are equal. -/
268 lemma hom_ext (h : is_colimit t) {W : C} {f f' : t.X ⟶ W}
id └────────┘ ┴ ┴ ┴└┘ ┴ ┴
src └────────┘ └┘ ┴
typ └────────┘ ┴ ┴ ┴└┘ ┴ ┴
doc └────────┘
269 (w : ∀ j, t.ι.app j ≫ f = t.ι.app j ≫ f') : f = f' :=
id ┴ ┴└┘└──┘ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ └┘ ┴ ┴ └┘
src └┘└──┘ ┴ ┴ └┘└──┘ ┴ ┴
typ ┴ ┴└┘└──┘ ┴ ┴ ┴ ┴ ┴└┘└──┘ ┴ ┴ └┘ ┴ ┴ └┘
270 by rw [h.hom_desc f, h.hom_desc f']; congr; exact funext w
id └────────┘ ┴ └────────┘ └┘ └────┘ ┴
src └──┘└────────┘┴ └┘└────────┘┴ ┴ └───┘ └────┘└────┘┴ └
typ └──┘└────────┘┴┴└┘└────────┘┴└┘┴ └───┘ └────┘└────┘┴┴└
doc └──┘ ┴ └┘ ┴ ┴ └────┘ ┴ └
txt └──┘ ┴ └┘ ┴ ┴ └───┘ └────┘ ┴ └
par └──┘ ┴ └┘ ┴ ┴ └───┘ └────┘ ┴ └
pid └┘ ┴ └┘ ┴ ┴ ┴ ┴ └
st └───────────────┘└─────────────┘┴└───────────────────────
271
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
272 /-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
273 a cocone on `F` with vertex `W`. -/
274 def hom_iso (h : is_colimit t) (W : C) : (t.X ⟶ W) ≅ (F ⟶ (const J).obj W) :=
id └────────┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴
src └────────┘ └┘ ┴ ┴ ┴ └───┘ └─┘
typ └────────┘ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴
doc └────────┘
275 { hom := λ f, (t.extend f).ι,
id ┴ ┴ ┴└─────┘ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ ┴└─────┘ ┴ ┴
doc ┴ └─────┘
276 inv := λ ι, h.desc { X := W, ι := ι },
id ┴ ┴└───┘ ┴ ┴
src └───┘
typ ┴ ┴└───┘ ┴ ┴
277 hom_inv_id' := by ext f; apply h.hom_ext; intro j; simp; dsimp; refl }
src └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
typ └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
doc └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
txt └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
par └───┘ └────┘ └─────┘ └──┘ └───┘ └───┘
pid └┘ ┴ └┘ ┴
st └──────────────────────────────────────────────────┘
278
279 @[simp] lemma hom_iso_hom (h : is_colimit t) {W : C} (f : t.X ⟶ W) :
id └────────┘ ┴ ┴ ┴└┘ ┴ ┴
src └────────┘ └┘ ┴
typ └────────┘ ┴ ┴ ┴└┘ ┴ ┴
doc └──┘ └────────┘
280 (is_colimit.hom_iso h W).hom f = (t.extend f).ι := rfl
id └────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴└─────┘ ┴ ┴ └─┘
src └────────────────┘ └─┘ ┴ └─────┘ ┴ └─┘
typ └────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴└─────┘ ┴ ┴ └─┘
doc └────────────────┘ └─────┘
281
282 /-- The colimit of `F` represents the functor taking `W` to
283 the set of cocones on `F` with vertex `W`. -/
284 def nat_iso (h : is_colimit t) : coyoneda.obj (op t.X) ≅ F.cocones :=
id └────────┘ ┴ └──────┘└──┘ └┘ ┴└┘ ┴ ┴└──────┘
src └────────┘ └──────┘└──┘ └┘ └┘ ┴ └──────┘
typ └────────┘ ┴ └──────┘└──┘ └┘ ┴└┘ ┴ ┴└──────┘
doc └────────┘ └──────┘
285 nat_iso.of_components (is_colimit.hom_iso h) (by intros; ext; dsimp; rw ←assoc; refl)
id └───────────────────┘ └────────────────┘ ┴ └───┘
src └───────────────────┘ └────────────────┘ └────┘ └─┘ └───┘ └──┘└───┘ └──┘
typ └───────────────────┘ └────────────────┘ ┴ └────┘ └─┘ └───┘ └──┘└───┘ └──┘
doc └────────────────┘ └────┘ └─┘ └───┘ └──┘ └──┘
txt └────┘ └─┘ └───┘ └──┘ └──┘
par └────┘ └─┘ └───┘ └──┘ └──┘
pid └┘
st └──────────────────────────────────┘
286
287 def hom_iso' (h : is_colimit t) (W : C) :
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
doc └────────┘
288 ((t.X ⟶ W) : Type v) ≅ { p : Π j, F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
id ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
typ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
289 h.hom_iso W ≪≫
id ┴└──────┘ ┴ └┘
src └──────┘ └┘
typ ┴└──────┘ ┴ └┘
doc └──────┘
290 { hom := λ ι,
id ┴ ┴
src ┴
typ ┴ ┴
doc ┴
291 ⟨λ j, ι.app j, λ j j' f,
id ┴ ┴└──┘ ┴ ┴ └┘ ┴
src └──┘
typ ┴ ┴└──┘ ┴ ┴ └┘ ┴
292 by convert ←(ι.naturality f); apply comp_id⟩,
id └──────────┘ ┴ └─────┘
src └───────┘ └──────────┘┴ ┴ └────┘└─────┘
typ └───────┘ └──────────┘┴┴┴ └────┘└─────┘
doc └───────┘ ┴ ┴ └────┘
txt └───────┘ ┴ ┴ └────┘
par └───────┘ ┴ ┴ └────┘
pid └┘ ┴ ┴ ┴
st └───────────────────────────────────────┘
293 inv := λ p,
id ┴
typ ┴
294 { app := λ j, p.1 j,
id ┴ ┴┴ ┴
src ┴
typ ┴ ┴┴ ┴
295 naturality' := λ j j' f, begin dsimp, rw [comp_id], exact (p.2 f) end } }
id ┴ └┘ ┴ └─────┘ ┴ ┴
src └───┘ └──┘└─────┘┴ └────┘ └─┘ └┘
typ ┴ └┘ ┴ └───┘ └──┘└─────┘┴ └────┘ ┴└─┘┴└┘
doc └───┘ └──┘ ┴ └────┘ └─┘ └┘
txt └───┘ └──┘ ┴ └────┘ └─┘ └┘
par └───┘ └──┘ ┴ └────┘ └─┘ └┘
pid └┘ ┴ ┴ └─┘ ┴┴
st └─────────┘└───────────┘└───────────────┘└─┘
296
297 /-- If G : C → D is a faithful functor which sends t to a colimit cocone,
298 then it suffices to check that the induced maps for the image of t
299 can be lifted to maps of C. -/
300 def of_faithful {t : cocone F} {D : Type u'} [category.{v} D] (G : C ⥤ D) [faithful G]
id └────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └────┘ └──────┘ ┴ └──────┘
typ └────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └────┘ └──────┘ ┴ └──────┘
301 (ht : is_colimit (G.map_cocone t)) (desc : Π (s : cocone F), t.X ⟶ s.X)
id └────────┘ ┴└─────────┘ ┴ └────┘ ┴ ┴└┘ ┴ ┴└┘
src └────────┘ └─────────┘ └────┘ └┘ ┴ └┘
typ └────────┘ ┴└─────────┘ ┴ └────┘ ┴ ┴└┘ ┴ ┴└┘
doc └────────┘ └─────────┘ └────┘
302 (h : ∀ s, G.map (desc s) = ht.desc (G.map_cocone s)) : is_colimit t :=
id ┴ ┴└──┘ └──┘ ┴ ┴ └┘└───┘ ┴└─────────┘ ┴ └────────┘ ┴
src └──┘ ┴ └───┘ └─────────┘ └────────┘
typ ┴ ┴└──┘ └──┘ ┴ ┴ └┘└───┘ ┴└─────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
303 { desc := desc,
id └──┘
typ └──┘
304 fac' := λ s j, by apply G.injectivity; rw [G.map_comp, h]; apply ht.fac,
id ┴ ┴ ┴
src └────┘ └──┘ └┘ ┴ └────┘
typ ┴ ┴ └────┘ └──┘└────────┘└┘┴┴ └────┘
doc └────┘ └──┘ └┘ ┴ └────┘
txt └────┘ └──┘ └┘ ┴ └────┘
par └────┘ └──┘ └┘ ┴ └────┘
pid ┴ └┘ └┘ ┴ ┴
st └────────────────────────┘└────────┘└─┘┴└────────────┘
305 uniq' := λ s m w, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └─────
306 apply G.injectivity, rw h,
id ┴
src └────┘ └─┘
typ └────┘ └─┘┴
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ ┴
st ──────────────────────┘└────┘└─
307 refine ht.uniq (G.map_cocone s) _ (λ j, _),
id └─────┘ └──────────┘ ┴
src └─────┘ ┴ └──────────┘┴ └──┘ └────┘
typ └─────┘└─────┘┴ └──────────┘┴┴└──┘ └────┘
doc └─────┘ ┴ └──────────┘┴ └──┘ └────┘
txt └─────┘ ┴ ┴ └──┘ └────┘
par └─────┘ ┴ ┴ └──┘ └────┘
pid ┴ ┴ ┴ └──┘ └────┘
st ─────────────────────────────────────────────┘└─
308 convert ←congr_arg (λ f, G.map f) (w j),
id └───────┘ └───┘ ┴ ┴
src └───────┘└───────┘┴ └──┘└───┘┴ └┘ ┴ ┴
typ └───────┘└───────┘┴ └──┘└───┘┴ └┘ ┴┴┴┴
doc └───────┘ ┴ └──┘ ┴ └┘ ┴ ┴
txt └───────┘ ┴ └──┘ ┴ └┘ ┴ ┴
par └───────┘ ┴ └──┘ ┴ └┘ ┴ ┴
pid └┘ ┴ └──┘ ┴ └┘ ┴ ┴
st ──────────────────────────────────────────┘└─
309 apply G.map_comp
src └────┘ └
typ └────┘ └
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────
310 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
311
312 def iso_unique_cocone_morphism {t : cocone F} :
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
313 is_colimit t ≅ Π s, unique (t ⟶ s) :=
id └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────────┘ ┴ └────┘ ┴
typ └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────────┘
314 { hom := λ h s,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
315 { default := h.desc_cocone_morphism s,
id ┴└───────────────────┘ ┴
src └───────────────────┘
typ ┴└───────────────────┘ ┴
316 uniq := λ _, h.uniq_cocone_morphism },
id ┴ ┴└───────────────────┘
src └───────────────────┘
typ ┴ ┴└───────────────────┘
317 inv := λ h,
id ┴
typ ┴
318 { desc := λ s, (h s).default.hom,
id ┴ ┴ ┴ ┴ └─────┘ └─┘
src ┴ └─────┘ └─┘
typ ┴ ┴ ┴ ┴ └─────┘ └─┘
doc ┴
319 uniq' := λ s f w, congr_arg cocone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
id ┴ ┴ ┴ └───────┘ └─────────────────┘ ┴ ┴ └──┘ ┴ ┴
src └───────┘ └─────────────────┘ └──┘
typ ┴ ┴ ┴ └───────┘ └─────────────────┘ ┴ ┴ └──┘ ┴ ┴
320
321 namespace of_nat_iso
322 variables {X : C} (h : coyoneda.obj (op X) ≅ F.cocones)
id └──────┘└──┘ └┘ ┴ └──────┘
src └──────┘└──┘ └┘ ┴ └──────┘
typ └──────┘└──┘ └┘ ┴ └──────┘
doc └──────┘
323
324 /-- If `F.cocones` is corepresented by `X`, each morphism `f : X ⟶ Y` gives a cocone with cone point `Y`. -/
325 def cocone_of_hom {Y : C} (f : X ⟶ Y) : cocone F :=
id ┴ ┴ ┴ ┴ └────┘ ┴
src ┴ └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
doc └────┘
326 { X := Y, ι := h.hom.app Y f }
id ┴ ┴└──┘└──┘ ┴ ┴
src └──┘└──┘
typ ┴ ┴└──┘└──┘ ┴ ┴
327
328 /-- If `F.cocones` is corepresented by `X`, each cocone `s` gives a morphism `X ⟶ s.X`. -/
329 def hom_of_cocone (s : cocone F) : X ⟶ s.X := h.inv.app s.X s.ι
id └────┘ ┴ ┴ ┴ ┴└┘ ┴└──┘└──┘ ┴└┘ ┴└┘
src └────┘ ┴ └┘ └──┘└──┘ └┘ └┘
typ └────┘ ┴ ┴ ┴ ┴└┘ ┴└──┘└──┘ ┴└┘ ┴└┘
doc └────┘
330
331 @[simp] lemma cocone_of_hom_of_cocone (s : cocone F) : cocone_of_hom h (hom_of_cocone h s) = s :=
id └────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └────┘ └───────────┘ └───────────┘ ┴
typ └────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └──┘ └────┘ └───────────┘ └───────────┘
332 begin
st └─────
333 dsimp [cocone_of_hom, hom_of_cocone], cases s, congr, dsimp,
id └───────────┘ └───────────┘ ┴
src └─────┘└───────────┘└┘└───────────┘┴ └────┘ └───┘ └───┘
typ └─────┘└───────────┘└┘└───────────┘┴ └────┘┴ └───┘ └───┘
doc └─────┘└───────────┘└┘└───────────┘┴ └────┘ └───┘
txt └─────┘ └┘ ┴ └────┘ └───┘ └───┘
par └─────┘ └┘ ┴ └────┘ └───┘ └───┘
pid ┴┴ └┘ ┴ ┴
st ─────────────────────────────────────┘└───────┘└─────┘└─────┘└─
334 exact congr_fun (congr_fun (congr_arg nat_trans.app h.inv_hom_id) s_X) s_ι,
id └───────┘ └───────┘ └───────────┘ └──────────┘ └─┘ └─┘
src └────┘ ┴ └───────┘┴ └───────┘┴└───────────┘┴└──────────┘└┘ └┘
typ └────┘ ┴ └───────┘┴ └───────┘┴└───────────┘┴└──────────┘└┘└─┘└┘└─┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └┘
st ───────────────────────────────────────────────────────────────────────────┘└─
335 end
st ──┘
336
337 @[simp] lemma hom_of_cocone_of_hom {Y : C} (f : X ⟶ Y) : hom_of_cocone h (cocone_of_hom h f) = f :=
id ┴ ┴ ┴ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
src ┴ └───────────┘ └───────────┘ ┴
typ ┴ ┴ ┴ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └──┘ └───────────┘ └───────────┘
338 congr_fun (congr_fun (congr_arg nat_trans.app h.hom_inv_id) Y) f
id └───────┘ └───────┘ └───────┘ └───────────┘ ┴└─────────┘ ┴ ┴
src └───────┘ └───────┘ └───────┘ └───────────┘ └─────────┘
typ └───────┘ └───────┘ └───────┘ └───────────┘ ┴└─────────┘ ┴ ┴
339
340 /-- If `F.cocones` is corepresented by `X`, the cocone corresponding to the identity morphism on `X`
341 will be a colimit cocone. -/
342 def colimit_cocone : cocone F :=
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
343 cocone_of_hom h (𝟙 X)
id └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴
doc └───────────┘
344
345 /-- If `F.cocones` is corepresented by `X`, the cocone corresponding to a morphism `f : Y ⟶ X` is
346 the colimit cocone extended by `f`. -/
347 lemma cocone_of_hom_fac {Y : C} (f : X ⟶ Y) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
348 cocone_of_hom h f = (colimit_cocone h).extend f :=
id └───────────┘ ┴ ┴ ┴ └────────────┘ ┴ └────┘ ┴
src └───────────┘ ┴ └────────────┘ └────┘
typ └───────────┘ ┴ ┴ ┴ └────────────┘ ┴ └────┘ ┴
doc └───────────┘ └────────────┘ └────┘
349 begin
st └─────
350 dsimp [cocone_of_hom, colimit_cocone, cocone.extend],
id └───────────┘ └────────────┘ └───────────┘
src └─────┘└───────────┘└┘└────────────┘└┘└───────────┘┴
typ └─────┘└───────────┘└┘└────────────┘└┘└───────────┘┴
doc └─────┘└───────────┘└┘└────────────┘└┘└───────────┘┴
txt └─────┘ └┘ └┘ ┴
par └─────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st ─────────────────────────────────────────────────────┘└─
351 congr,
src └───┘
typ └───┘
txt └───┘
par └───┘
st ──────┘└─
352 ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
353 have t := congr_fun (h.hom.naturality f) (𝟙 X),
id └───────┘ └──────────────┘ ┴ ┴ ┴
src └────────┘└───────┘┴ └──────────────┘┴ └┘ ┴┴ ┴
typ └────────┘└───────┘┴ └──────────────┘┴┴└┘ ┴┴┴┴
doc └────────┘ ┴ ┴ └┘ ┴ ┴
txt └────────┘ ┴ ┴ └┘ ┴ ┴
par └────────┘ ┴ ┴ └┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────┘└─
354 dsimp at t,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└──┘
st ───────────┘└─
355 simp only [id_comp] at t,
id └─────┘
src └─────────┘└─────┘└────┘
typ └─────────┘└─────┘└────┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid ┴└──┘└┘ ┴┴└──┘
st ─────────────────────────┘└─
356 rw congr_fun (congr_arg nat_trans.app t) j,
id └───────┘ └───────┘ └───────────┘ ┴ ┴
src └─┘└───────┘┴ └───────┘┴└───────────┘┴ └┘
typ └─┘└───────┘┴ └───────┘┴└───────────┘┴┴└┘┴
doc └─┘ ┴ ┴ ┴ └┘
txt └─┘ ┴ ┴ ┴ └┘
par └─┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────┘└─
357 refl,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ─────┘└─
358 end
st ──┘
359
360 /-- If `F.cocones` is corepresented by `X`, any cocone is the extension of the colimit cocone by the
361 corresponding morphism. -/
362 lemma cocone_fac (s : cocone F) : (colimit_cocone h).extend (hom_of_cocone h s) = s :=
id └────┘ ┴ └────────────┘ ┴ └────┘ └───────────┘ ┴ ┴ ┴ ┴
src └────┘ └────────────┘ └────┘ └───────────┘ ┴
typ └────┘ ┴ └────────────┘ ┴ └────┘ └───────────┘ ┴ ┴ ┴ ┴
doc └────┘ └────────────┘ └────┘ └───────────┘
363 begin
st └─────
364 rw ←cocone_of_hom_of_cocone h s,
id └─────────────────────┘ ┴ ┴
src └──┘└─────────────────────┘┴ ┴
typ └──┘└─────────────────────┘┴┴┴┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ────────────────────────────────┘└─
365 conv_lhs { simp only [hom_of_cocone_of_hom] },
id └──────────────────┘
src └─────────┘└─────────┘└──────────────────┘└┘┴
typ └─────────┘└─────────┘└──────────────────┘└┘┴
txt └─────────┘└─────────┘ └┘┴
par └─────────┘└─────────┘ └┘┴
pid ┴└───────────┘ └─┘
st ───────────┘└────────────────────────────────┘└┘└
366 apply (cocone_of_hom_fac _ _).symm,
id └───────────────┘
src └────┘ └───────────────┘└────────┘
typ └────┘ └───────────────┘└────────┘
doc └────┘ └───────────────┘└────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └───────┘┴
st ───────────────────────────────────┘└─
367 end
st ──┘
368
369 end of_nat_iso
370
371 section
372 open of_nat_iso
373
374 /--
375 If `F.cocones` is corepresentable, then the cocone corresponding to the identity morphism on
376 the representing object is a colimit cocone.
377 -/
378 def of_nat_iso {X : C} (h : coyoneda.obj (op X) ≅ F.cocones) :
id ┴ └──────┘└──┘ └┘ ┴ ┴ ┴└──────┘
src └──────┘└──┘ └┘ ┴ └──────┘
typ ┴ └──────┘└──┘ └┘ ┴ ┴ ┴└──────┘
doc └──────┘
379 is_colimit (colimit_cocone h) :=
id └────────┘ └────────────┘ ┴
src └────────┘ └────────────┘
typ └────────┘ └────────────┘ ┴
doc └────────┘ └────────────┘
380 { desc := λ s, hom_of_cocone h s,
id ┴ └───────────┘ ┴ ┴
src └───────────┘
typ ┴ └───────────┘ ┴ ┴
doc └───────────┘
381 fac' := λ s j,
id ┴ ┴
typ ┴ ┴
382 begin
st └─────
383 have h := cocone_fac h s,
id └────────┘ ┴ ┴
src └────────┘└────────┘┴ ┴
typ └────────┘└────────┘┴┴┴┴
doc └────────┘└────────┘┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ───────────────────────────┘└─
384 cases s,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────┘└─
385 injection h with h₁ h₂,
id ┴
src └────────┘ └─────────┘
typ └────────┘┴└─────────┘
doc └────────┘ └─────────┘
txt └────────┘ └─────────┘
par └────────┘ └─────────┘
pid ┴ └─────────┘
st ─────────────────────────┘└─
386 simp only [heq_iff_eq] at h₂,
id └────────┘
src └─────────┘└────────┘└─────┘
typ └─────────┘└────────┘└─────┘
doc └─────────┘ └─────┘
txt └─────────┘ └─────┘
par └─────────┘ └─────┘
pid ┴└──┘└┘ ┴┴└───┘
st ───────────────────────────────┘└─
387 conv_rhs { rw ← h₂ }, refl,
id └┘
src └─────────┘└───┘ ┴┴ └──┘
typ └─────────┘└───┘└┘┴┴ └──┘
doc └──┘
txt └─────────┘└───┘ ┴┴ └──┘
par └─────────┘└───┘ ┴┴ └──┘
pid ┴└─────┘ └┘
st ─────────────┘└───────┘└┘└───┘└─
388 end,
st ────┘
389 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
390 begin
st └─────
391 rw ←hom_of_cocone_of_hom h m,
id └──────────────────┘ ┴ ┴
src └──┘└──────────────────┘┴ ┴
typ └──┘└──────────────────┘┴┴┴┴
doc └──┘ ┴ ┴
txt └──┘ ┴ ┴
par └──┘ ┴ ┴
pid └┘ ┴ ┴
st ───────────────────────────────┘└─
392 congr,
src └───┘
typ └───┘
txt └───┘
par └───┘
st ────────┘└─
393 rw cocone_of_hom_fac,
id └───────────────┘
src └─┘└───────────────┘
typ └─┘└───────────────┘
doc └─┘└───────────────┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
394 dsimp, cases s, congr,
id ┴
src └───┘ └────┘ └───┘
typ └───┘ └────┘┴ └───┘
doc └───┘ └────┘
txt └───┘ └────┘ └───┘
par └───┘ └────┘ └───┘
pid ┴
st ────────┘└───────┘└─────┘└─
395 ext j, exact w j,
id ┴ ┴
src └───┘ └────┘ ┴
typ └───┘ └────┘┴┴┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid └┘ ┴ ┴
st ────────┘└─────────┘└─
396 end }
st ────┘
397 end
398
399 end is_colimit
400
401 section limit
402
403 /-- `has_limit F` represents a particular chosen limit of the diagram `F`. -/
404 class has_limit (F : J ⥤ C) :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
405 (cone : cone F)
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘
406 (is_limit : is_limit cone . tactic.apply_instance)
id └──────┘ └──┘ ┴
src └──────┘
typ └──────┘ └──┘ ┴
doc └──────┘
407
408 variables (J C)
409
410 /-- `C` has limits of shape `J` if we have chosen a particular limit of
411 every functor `F : J ⥤ C`. -/
412 class has_limits_of_shape :=
413 (has_limit : Π F : J ⥤ C, has_limit F)
id ┴ ┴ ┴ ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ ┴ ┴ ┴ └───────┘ ┴
doc ┴ └───────┘
414
415 /-- `C` has all (small) limits if it has limits of every shape. -/
416 class has_limits :=
417 (has_limits_of_shape : Π (J : Type v) [𝒥 : small_category J], has_limits_of_shape J C)
id ┴ └──┘ └────────────┘ ┴ └─────────────────┘ ┴ ┴
src └────────────┘ └─────────────────┘
typ ┴ └──┘ └────────────┘ ┴ └─────────────────┘ ┴ ┴
doc └────────────┘ └─────────────────┘
418
419 variables {J C}
420
421 @[priority 100] -- see Note [lower instance priority]
422 instance has_limit_of_has_limits_of_shape
423 {J : Type v} [small_category J] [H : has_limits_of_shape J C] (F : J ⥤ C) : has_limit F :=
id └────────────┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
src └────────────┘ └─────────────────┘ ┴ └───────┘
typ └────────────┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
doc └────────────┘ └─────────────────┘ ┴ └───────┘
424 has_limits_of_shape.has_limit F
id └───────────────────────────┘ ┴
src └───────────────────────────┘
typ └───────────────────────────┘ ┴
425
426 @[priority 100] -- see Note [lower instance priority]
427 instance has_limits_of_shape_of_has_limits
428 {J : Type v} [small_category J] [H : has_limits.{v} C] : has_limits_of_shape J C :=
id └────────────┘ ┴ └────────┘ ┴ └─────────────────┘ ┴ ┴
src └────────────┘ └────────┘ └─────────────────┘
typ └────────────┘ ┴ └────────┘ ┴ └─────────────────┘ ┴ ┴
doc └────────────┘ └────────┘ └─────────────────┘
429 has_limits.has_limits_of_shape C J
id └────────────────────────────┘ ┴ ┴
src └────────────────────────────┘
typ └────────────────────────────┘ ┴ ┴
430
431 /- Interface to the `has_limit` class. -/
432
433 def limit.cone (F : J ⥤ C) [has_limit F] : cone F := has_limit.cone F
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ └────────────┘ ┴
src ┴ └───────┘ └──┘ └────────────┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ └────────────┘ ┴
doc ┴ └───────┘ └──┘
434
435 def limit (F : J ⥤ C) [has_limit F] := (limit.cone F).X
id ┴ ┴ ┴ └───────┘ ┴ └────────┘ ┴ ┴
src ┴ └───────┘ └────────┘ ┴
typ ┴ ┴ ┴ └───────┘ ┴ └────────┘ ┴ ┴
doc ┴ └───────┘
436
437 def limit.π (F : J ⥤ C) [has_limit F] (j : J) : limit F ⟶ F.obj j :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ └───┘ ┴ ┴ ┴└──┘ ┴
src ┴ └───────┘ └───┘ ┴ └──┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ └───┘ ┴ ┴ ┴└──┘ ┴
doc ┴ └───────┘
438 (limit.cone F).π.app j
id └────────┘ ┴ ┴ └─┘ ┴
src └────────┘ ┴ └─┘
typ └────────┘ ┴ ┴ └─┘ ┴
439
440 @[simp] lemma limit.cone_π {F : J ⥤ C} [has_limit F] (j : J) :
id ┴ ┴ ┴ └───────┘ ┴ ┴
src ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └──┘ ┴ └───────┘
441 (limit.cone F).π.app j = limit.π _ j := rfl
id └────────┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ └─┘
src └────────┘ ┴ └─┘ ┴ └─────┘ └─┘
typ └────────┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ └─┘
442
443 @[simp] lemma limit.w (F : J ⥤ C) [has_limit F] {j j' : J} (f : j ⟶ j') :
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘
src ┴ └───────┘ ┴
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └┘
doc └──┘ ┴ └───────┘
444 limit.π F j ≫ F.map f = limit.π F j' := (limit.cone F).w f
id └─────┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ └─────┘ ┴ └┘ └────────┘ ┴ ┴ ┴
src └─────┘ ┴ └──┘ ┴ └─────┘ └────────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ └─────┘ ┴ └┘ └────────┘ ┴ ┴ ┴
445
446 def limit.is_limit (F : J ⥤ C) [has_limit F] : is_limit (limit.cone F) :=
id ┴ ┴ ┴ └───────┘ ┴ └──────┘ └────────┘ ┴
src ┴ └───────┘ └──────┘ └────────┘
typ ┴ ┴ ┴ └───────┘ ┴ └──────┘ └────────┘ ┴
doc ┴ └───────┘ └──────┘
447 has_limit.is_limit.{v} F
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
448
449 def limit.lift (F : J ⥤ C) [has_limit F] (c : cone F) : c.X ⟶ limit F :=
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴└┘ ┴ └───┘ ┴
src ┴ └───────┘ └──┘ └┘ ┴ └───┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴└┘ ┴ └───┘ ┴
doc ┴ └───────┘ └──┘
450 (limit.is_limit F).lift c
id └────────────┘ ┴ └──┘ ┴
src └────────────┘ └──┘
typ └────────────┘ ┴ └──┘ ┴
451
452 @[simp] lemma limit.is_limit_lift {F : J ⥤ C} [has_limit F] (c : cone F) :
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴
src ┴ └───────┘ └──┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴
doc └──┘ ┴ └───────┘ └──┘
453 (limit.is_limit F).lift c = limit.lift F c := rfl
id └────────────┘ ┴ └──┘ ┴ ┴ └────────┘ ┴ ┴ └─┘
src └────────────┘ └──┘ ┴ └────────┘ └─┘
typ └────────────┘ ┴ └──┘ ┴ ┴ └────────┘ ┴ ┴ └─┘
454
455 @[simp, reassoc] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴
src ┴ └───────┘ └──┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴
doc └──┘ └─────┘ ┴ └───────┘ └──┘
456 limit.lift F c ≫ limit.π F j = c.π.app j :=
id └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴└┘└──┘ ┴
src └────────┘ ┴ └─────┘ ┴ └┘└──┘
typ └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴└┘└──┘ ┴
457 is_limit.fac _ c j
id └──────────┘ ┴ ┴
typ └──────────┘ ┴ ┴
458
459 def limit.cone_morphism {F : J ⥤ C} [has_limit F] (c : cone F) :
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴
src ┴ └───────┘ └──┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴
doc ┴ └───────┘ └──┘
460 cone_morphism c (limit.cone F) :=
id └───────────┘ ┴ └────────┘ ┴
src └───────────┘ └────────┘
typ └───────────┘ ┴ └────────┘ ┴
461 (limit.is_limit F).lift_cone_morphism c
id └────────────┘ ┴ └────────────────┘ ┴
src └────────────┘ └────────────────┘
typ └────────────┘ ┴ └────────────────┘ ┴
462
463 @[simp] lemma limit.cone_morphism_hom {F : J ⥤ C} [has_limit F] (c : cone F) :
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴
src ┴ └───────┘ └──┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴
doc └──┘ ┴ └───────┘ └──┘
464 (limit.cone_morphism c).hom = limit.lift F c := rfl
id └─────────────────┘ ┴ └─┘ ┴ └────────┘ ┴ ┴ └─┘
src └─────────────────┘ └─┘ ┴ └────────┘ └─┘
typ └─────────────────┘ ┴ └─┘ ┴ └────────┘ ┴ ┴ └─┘
465 @[simp] lemma limit.cone_morphism_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴
src ┴ └───────┘ └──┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴
doc └──┘ ┴ └───────┘ └──┘
466 (limit.cone_morphism c).hom ≫ limit.π F j = c.π.app j :=
id └─────────────────┘ ┴ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴└┘└──┘ ┴
src └─────────────────┘ └─┘ ┴ └─────┘ ┴ └┘└──┘
typ └─────────────────┘ ┴ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴└┘└──┘ ┴
467 by erw is_limit.fac
id └──────────┘
src └──┘ └
typ └──┘└──────────┘└
doc └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └─────────────────
468
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
469 @[ext] lemma limit.hom_ext {F : J ⥤ C} [has_limit F] {X : C} {f f' : X ⟶ limit F}
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴
src ┴ └───────┘ ┴ └───┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴
doc └─┘ ┴ └───────┘
470 (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) : f = f' :=
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └┘
src ┴ └─────┘ ┴ ┴ └─────┘ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └┘
471 (limit.is_limit F).hom_ext w
id └────────────┘ ┴ └─────┘ ┴
src └────────────┘ └─────┘
typ └────────────┘ ┴ └─────┘ ┴
doc └─────┘
472
473 def limit.hom_iso (F : J ⥤ C) [has_limit F] (W : C) : (W ⟶ limit F) ≅ (F.cones.obj (op W)) :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴└────┘└──┘ └┘ ┴
src ┴ └───────┘ ┴ └───┘ ┴ └────┘└──┘ └┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴└────┘└──┘ └┘ ┴
doc ┴ └───────┘ └────┘
474 (limit.is_limit F).hom_iso W
id └────────────┘ ┴ └─────┘ ┴
src └────────────┘ └─────┘
typ └────────────┘ ┴ └─────┘ ┴
doc └─────┘
475
476 @[simp] lemma limit.hom_iso_hom (F : J ⥤ C) [has_limit F] {W : C} (f : W ⟶ limit F) :
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴
src ┴ └───────┘ ┴ └───┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───┘ ┴
doc └──┘ ┴ └───────┘
477 (limit.hom_iso F W).hom f = (const J).map f ≫ (limit.cone F).π :=
id └───────────┘ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └────────┘ ┴ ┴
src └───────────┘ └─┘ ┴ └───┘ └─┘ ┴ └────────┘ ┴
typ └───────────┘ ┴ ┴ └─┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └────────┘ ┴ ┴
478 (limit.is_limit F).hom_iso_hom f
id └────────────┘ ┴ └─────────┘ ┴
src └────────────┘ └─────────┘
typ └────────────┘ ┴ └─────────┘ ┴
479
480 def limit.hom_iso' (F : J ⥤ C) [has_limit F] (W : C) :
id ┴ ┴ ┴ └───────┘ ┴ ┴
src ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴
doc ┴ └───────┘
481 ((W ⟶ limit F) : Type v) ≅ { p : Π j, W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ └┘
src ┴ └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ └┘
482 (limit.is_limit F).hom_iso' W
id └────────────┘ ┴ └──────┘ ┴
src └────────────┘ └──────┘
typ └────────────┘ ┴ └──────┘ ┴
483
484 lemma limit.lift_extend {F : J ⥤ C} [has_limit F] (c : cone F) {X : C} (f : X ⟶ c.X) :
id ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴└┘
src ┴ └───────┘ └──┘ ┴ └┘
typ ┴ ┴ ┴ └───────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴└┘
doc ┴ └───────┘ └──┘
485 limit.lift F (c.extend f) = f ≫ limit.lift F c :=
id └────────┘ ┴ ┴└─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────┘ └─────┘ ┴ ┴ └────────┘
typ └────────┘ ┴ ┴└─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └─────┘
486 by obviously
id └───────┘
src └───────┘
typ └───────┘
doc └───────┘
par └───────┘
st └────────┘
487
488 def has_limit_of_iso {F G : J ⥤ C} [has_limit F] (α : F ≅ G) : has_limit G :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
src ┴ └───────┘ ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
doc ┴ └───────┘ └───────┘
489 { cone := (cones.postcompose α.hom).obj (limit.cone F),
id └───────────────┘ ┴└──┘ └─┘ └────────┘ ┴
src └───────────────┘ └──┘ └─┘ └────────┘
typ └───────────────┘ ┴└──┘ └─┘ └────────┘ ┴
490 is_limit :=
491 { lift := λ s, limit.lift F ((cones.postcompose α.inv).obj s),
id ┴ └────────┘ ┴ └───────────────┘ ┴└──┘ └─┘ ┴
src └────────┘ └───────────────┘ └──┘ └─┘
typ ┴ └────────┘ ┴ └───────────────┘ ┴└──┘ └─┘ ┴
492 fac' := λ s j,
id ┴ ┴
typ ┴ ┴
493 begin
st └─────
494 rw [cones.postcompose_obj_π, nat_trans.comp_app, limit.cone_π, ←category.assoc, limit.lift_π],
id └─────────────────────┘ └────────────────┘ └──────────┘ └────────────┘ └──────────┘
src └──┘└─────────────────────┘└┘└────────────────┘└┘└──────────┘└─┘└────────────┘└┘└──────────┘┴
typ └──┘└─────────────────────┘└┘└────────────────┘└┘└──────────┘└─┘└────────────┘└┘└──────────┘┴
doc └──┘ └┘ └┘ └─┘ └┘ ┴
txt └──┘ └┘ └┘ └─┘ └┘ ┴
par └──┘ └┘ └┘ └─┘ └┘ ┴
pid └┘ └┘ └┘ └─┘ └┘ ┴
st ────────────────────────────────┘└──────────────────┘└────────────┘└───────────────┘└────────────┘└──
495 simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st ───────────
496 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
497 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
498 begin
st └─────
499 apply limit.hom_ext, intro j,
id └───────────┘
src └────┘└───────────┘ └─────┘
typ └────┘└───────────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ────────────────────────┘└───────┘└─
500 rw [limit.lift_π, cones.postcompose_obj_π, nat_trans.comp_app, ←nat_iso.app_inv, iso.eq_comp_inv],
id └──────────┘ └─────────────────────┘ └────────────────┘ └─────────────┘ └─────────────┘
src └──┘└──────────┘└┘└─────────────────────┘└┘└────────────────┘└─┘└─────────────┘└┘└─────────────┘┴
typ └──┘└──────────┘└┘└─────────────────────┘└┘└────────────────┘└─┘└─────────────┘└┘└─────────────┘┴
doc └──┘ └┘ └┘ └─┘ └┘ ┴
txt └──┘ └┘ └┘ └─┘ └┘ ┴
par └──┘ └┘ └┘ └─┘ └┘ ┴
pid └┘ └┘ └┘ └─┘ └┘ ┴
st ─────────────────────┘└───────────────────────┘└──────────────────┘└────────────────┘└───────────────┘└──
501 simpa using w j
id ┴ ┴
src └──────────┘ ┴ └
typ └──────────┘┴┴┴└
doc └──────────┘ ┴ └
txt └──────────┘ ┴ └
par └──────────┘ ┴ └
pid ┴└────┘ ┴ └
st ──────────────────────
502 end } }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
503
504 /-- If a functor `G` has the same collection of cones as a functor `F`
505 which has a limit, then `G` also has a limit. -/
506 -- See the construction of limits from products and equalizers
507 -- for an example usage.
508 def has_limit.of_cones_iso {J K : Type v} [small_category J] [small_category K] (F : J ⥤ C) (G : K ⥤ C)
id └────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └────────────┘ ┴ ┴
typ └────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────┘ └────────────┘ ┴ ┴
509 (h : F.cones ≅ G.cones) [has_limit F] : has_limit G :=
id ┴└────┘ ┴ ┴└────┘ └───────┘ ┴ └───────┘ ┴
src └────┘ ┴ └────┘ └───────┘ └───────┘
typ ┴└────┘ ┴ ┴└────┘ └───────┘ ┴ └───────┘ ┴
doc └────┘ └────┘ └───────┘ └───────┘
510 ⟨_, is_limit.of_nat_iso ((is_limit.nat_iso (limit.is_limit F)) ≪≫ h)⟩
id └─────────────────┘ └──────────────┘ └────────────┘ ┴ └┘ ┴
src └─────────────────┘ └──────────────┘ └────────────┘ └┘
typ └─────────────────┘ └──────────────┘ └────────────┘ ┴ └┘ ┴
doc └─────────────────┘ └──────────────┘
511
512 section pre
513 variables (F) [has_limit F] (E : K ⥤ J) [has_limit (E ⋙ F)]
id └───────┘ ┴ └───────┘ ┴
src └───────┘ ┴ └───────┘ ┴
typ └───────┘ ┴ └───────┘ ┴
doc └───────┘ ┴ └───────┘ ┴
514
515 def limit.pre : limit F ⟶ limit (E ⋙ F) :=
id └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴
typ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc ┴
516 limit.lift (E ⋙ F)
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴
doc ┴
517 { X := limit F,
id └───┘ ┴
src └───┘
typ └───┘ ┴
518 π := { app := λ k, limit.π F (E.obj k) } }
id ┴ ┴ └─────┘ ┴ ┴└──┘ ┴
src ┴ └─────┘ └──┘
typ ┴ ┴ └─────┘ ┴ ┴└──┘ ┴
doc ┴
519
520 @[simp] lemma limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) :=
id ┴ └───────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──┘ ┴
src └───────┘ ┴ └─────┘ ┴ ┴ └─────┘ └──┘
typ ┴ └───────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──┘ ┴
doc └──┘ ┴
521 by erw is_limit.fac
id └──────────┘
src └──┘ └
typ └──┘└──────────┘└
doc └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └─────────────────
522
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
523 @[simp] lemma limit.lift_pre (c : cone F) :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘ └──┘
524 limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E) :=
id └────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└──────┘ ┴
src └────────┘ ┴ └───────┘ ┴ └────────┘ ┴ └──────┘
typ └────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└──────┘ ┴
doc ┴
525 by ext; simp
src └─┘ └────
typ └─┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid └
st └──────────
526
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
527 variables {L : Type v} [small_category L]
id └────────────┘
src └────────────┘
typ └────────────┘
doc └────────────┘
528 variables (D : L ⥤ K) [has_limit (D ⋙ E ⋙ F)]
id ┴ └───────┘ ┴ ┴
src ┴ └───────┘ ┴ ┴
typ ┴ └───────┘ ┴ ┴
doc ┴ └───────┘ ┴ ┴
529
530 @[simp] lemma limit.pre_pre : limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E) :=
id └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ ┴ └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
531 by ext j; erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]; refl
id └───┘ └─────────┘ └─────────┘ └─────────┘
src └───┘ └───┘└───┘└┘└─────────┘└┘└─────────┘└┘└─────────┘┴ └────
typ └───┘ └───┘└───┘└┘└─────────┘└┘└─────────┘└┘└─────────┘┴ └────
doc └───┘ └───┘ └┘ └┘ └┘ ┴ └────
txt └───┘ └───┘ └┘ └┘ └┘ ┴ └────
par └───┘ └───┘ └┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ └┘ └┘ ┴ └
st └───────────┘└───┘└───────────┘└───────────┘└───────────┘┴└──────
532
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
533 end pre
534
535 section post
536 variables {D : Type u'} [𝒟 : category.{v} D]
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
537 include 𝒟
538
539 variables (F) [has_limit F] (G : C ⥤ D) [has_limit (F ⋙ G)]
id └───────┘ ┴ └───────┘ ┴
src └───────┘ ┴ └───────┘ ┴
typ └───────┘ ┴ └───────┘ ┴
doc └───────┘ ┴ └───────┘ ┴
540
541 def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) :=
id ┴└──┘ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
src └──┘ └───┘ ┴ └───┘ ┴
typ ┴└──┘ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴
doc ┴
542 limit.lift (F ⋙ G)
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴
doc ┴
543 { X := G.obj (limit F),
id ┴└──┘ └───┘ ┴
src └──┘ └───┘
typ ┴└──┘ └───┘ ┴
544 π :=
545 { app := λ j, G.map (limit.π F j),
id ┴ ┴└──┘ └─────┘ ┴ ┴
src └──┘ └─────┘
typ ┴ ┴└──┘ └─────┘ ┴ ┴
546 naturality' :=
547 by intros j j' f; erw [←G.map_comp, limits.cone.w, id_comp]; refl } }
id └───────────┘ └─────┘
src └───────────┘ └────┘ └┘└───────────┘└┘└─────┘┴ └───┘
typ └───────────┘ └────┘└────────┘└┘└───────────┘└┘└─────┘┴ └───┘
doc └───────────┘ └────┘ └┘ └┘ ┴ └───┘
txt └───────────┘ └────┘ └┘ └┘ ┴ └───┘
par └───────────┘ └────┘ └┘ └┘ ┴ └───┘
pid └─────┘ └─┘ └┘ └┘ ┴ ┴
st └───────────────────┘└─────────┘└─────────────┘└───────┘┴└─────┘
548
549 @[simp] lemma limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) :=
id ┴ └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └─────┘ ┴ ┴
src └────────┘ ┴ └─────┘ ┴ ┴ └──┘ └─────┘
typ ┴ └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └─────┘ ┴ ┴
doc └──┘ ┴
550 by erw is_limit.fac
id └──────────┘
src └──┘ └
typ └──┘└──────────┘└
doc └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └─────────────────
551
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
552 @[simp] lemma limit.lift_post (c : cone F) :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘ └──┘
553 G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.map_cone c) :=
id ┴└──┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└───────┘ ┴
src └──┘ └────────┘ ┴ └────────┘ ┴ └────────┘ ┴ └───────┘
typ ┴└──┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴└───────┘ ┴
doc ┴ └───────┘
554 by ext; rw [assoc, limit.post_π, ←G.map_comp, limit.lift_π, limit.lift_π]; refl
id └───┘ └──────────┘ └──────────┘ └──────────┘
src └─┘ └──┘└───┘└┘└──────────┘└─┘ └┘└──────────┘└┘└──────────┘┴ └────
typ └─┘ └──┘└───┘└┘└──────────┘└─┘└────────┘└┘└──────────┘└┘└──────────┘┴ └────
doc └─┘ └──┘ └┘ └─┘ └┘ └┘ ┴ └────
txt └─┘ └──┘ └┘ └─┘ └┘ └┘ ┴ └────
par └─┘ └──┘ └┘ └─┘ └┘ └┘ ┴ └────
pid └┘ └┘ └─┘ └┘ └┘ ┴ └
st └────────┘└───┘└────────────┘└───────────┘└────────────┘└────────────┘┴└──────
555
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
556 @[simp] lemma limit.post_post
doc └──┘
557 {E : Type u''} [category.{v} E] (H : D ⥤ E) [has_limit ((F ⋙ G) ⋙ H)] :
id └──────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └───────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ ┴ └───────┘ ┴ ┴
558 /- H G (limit F) ⟶ H (limit (F ⋙ G)) ⟶ limit ((F ⋙ G) ⋙ H) equals -/
559 /- H G (limit F) ⟶ limit (F ⋙ (G ⋙ H)) -/
560 H.map (limit.post F G) ≫ limit.post (F ⋙ G) H = limit.post F (G ⋙ H) :=
id ┴└──┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └──┘ └────────┘ ┴ └────────┘ ┴ ┴ └────────┘ ┴
typ ┴└──┘ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc ┴ ┴
561 by ext; erw [assoc, limit.post_π, ←H.map_comp, limit.post_π, limit.post_π]; refl
id └───┘ └──────────┘ └──────────┘ └──────────┘
src └─┘ └───┘└───┘└┘└──────────┘└─┘ └┘└──────────┘└┘└──────────┘┴ └────
typ └─┘ └───┘└───┘└┘└──────────┘└─┘└────────┘└┘└──────────┘└┘└──────────┘┴ └────
doc └─┘ └───┘ └┘ └─┘ └┘ └┘ ┴ └────
txt └─┘ └───┘ └┘ └─┘ └┘ └┘ ┴ └────
par └─┘ └───┘ └┘ └─┘ └┘ └┘ ┴ └────
pid └┘ └┘ └─┘ └┘ └┘ ┴ └
st └─────────┘└───┘└────────────┘└───────────┘└────────────┘└────────────┘┴└──────
562
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
563 end post
564
565 lemma limit.pre_post {D : Type u'} [category.{v} D]
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
566 (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴
567 [has_limit F] [has_limit (E ⋙ F)] [has_limit (F ⋙ G)] [has_limit ((E ⋙ F) ⋙ G)] :
id └───────┘ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ ┴
typ └───────┘ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ ┴
568 /- G (limit F) ⟶ G (limit (E ⋙ F)) ⟶ limit ((E ⋙ F) ⋙ G) vs -/
569 /- G (limit F) ⟶ limit F ⋙ G ⟶ limit (E ⋙ (F ⋙ G)) or -/
570 G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E :=
id ┴└──┘ └───────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └──┘ └───────┘ ┴ └────────┘ ┴ ┴ └────────┘ ┴ └───────┘ ┴
typ ┴└──┘ └───────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc ┴ ┴
571 by ext; erw [assoc, limit.post_π, ←G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]; refl
id └───┘ └──────────┘ └─────────┘ └───┘ └─────────┘ └──────────┘
src └─┘ └───┘└───┘└┘└──────────┘└─┘ └┘└─────────┘└┘└───┘└┘└─────────┘└┘└──────────┘┴ └────
typ └─┘ └───┘└───┘└┘└──────────┘└─┘└────────┘└┘└─────────┘└┘└───┘└┘└─────────┘└┘└──────────┘┴ └────
doc └─┘ └───┘ └┘ └─┘ └┘ └┘ └┘ └┘ ┴ └────
txt └─┘ └───┘ └┘ └─┘ └┘ └┘ └┘ └┘ ┴ └────
par └─┘ └───┘ └┘ └─┘ └┘ └┘ └┘ └┘ ┴ └────
pid └┘ └┘ └─┘ └┘ └┘ └┘ └┘ ┴ └
st └─────────┘└───┘└────────────┘└───────────┘└───────────┘└─────┘└───────────┘└────────────┘┴└──────
572
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
573 open category_theory.equivalence
574 instance has_limit_equivalence_comp (e : K ≌ J) [has_limit F] : has_limit (e.functor ⋙ F) :=
id ┴ ┴ ┴ └───────┘ ┴ └───────┘ ┴└──────┘ ┴ ┴
src ┴ └───────┘ └───────┘ └──────┘ ┴
typ ┴ ┴ ┴ └───────┘ ┴ └───────┘ ┴└──────┘ ┴ ┴
doc ┴ └───────┘ └───────┘ ┴
575 { cone := cone.whisker e.functor (limit.cone F),
id └──────────┘ ┴└──────┘ └────────┘ ┴
src └──────────┘ └──────┘ └────────┘
typ └──────────┘ ┴└──────┘ └────────┘ ┴
576 is_limit :=
577 let e' := cones.postcompose (e.inv_fun_id_assoc F).hom in
id └┘ └───────────────┘ ┴└───────────────┘ ┴ └─┘
src └───────────────┘ └───────────────┘ └─┘
typ └┘ └───────────────┘ ┴└───────────────┘ ┴ └─┘
578 { lift := λ s, limit.lift F (e'.obj (cone.whisker e.inverse s)),
id ┴ └────────┘ ┴ └┘└──┘ └──────────┘ ┴└──────┘ ┴
src └────────┘ └──┘ └──────────┘ └──────┘
typ ┴ └────────┘ ┴ └┘└──┘ └──────────┘ ┴└──────┘ ┴
579 fac' := λ s j,
id ┴ ┴
typ ┴ ┴
580 begin
st └─────
581 dsimp, rw [limit.lift_π], dsimp [e'],
id └──────────┘ └┘
src └───┘ └──┘└──────────┘┴ └─────┘ ┴
typ └───┘ └──┘└──────────┘┴ └─────┘└┘┴
doc └───┘ └──┘ ┴ └─────┘ ┴
txt └───┘ └──┘ ┴ └─────┘ ┴
par └───┘ └──┘ ┴ └─────┘ ┴
pid └┘ ┴ ┴┴ ┴
st ──────────┘└────────────────┘└───────────┘└─
582 erw [inv_fun_id_assoc_hom_app, counit_functor, ←s.π.naturality, id_comp]
id └──────────────────────┘ └────────────┘ └─────┘
src └───┘└──────────────────────┘└┘└────────────┘└─┘ └┘└─────┘└─
typ └───┘└──────────────────────┘└┘└────────────┘└─┘└────────────┘└┘└─────┘└─
doc └───┘ └┘ └─┘ └┘ └─
txt └───┘ └┘ └─┘ └┘ └─
par └───┘ └┘ └─┘ └┘ └─
pid └┘ └┘ └─┘ └┘ ┴└
st ──────────────────────────────────┘└──────────────┘└───────────────┘└───────┘┴└
583 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
584 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
585 begin
st └─────
586 apply limit.hom_ext, intro j,
id └───────────┘
src └────┘└───────────┘ └─────┘
typ └────┘└───────────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ────────────────────────┘└───────┘└─
587 erw [limit.lift_π, ←limit.w F (e.counit_iso.hom.app j)],
id └──────────┘ └─────┘ ┴ └──────────────────┘ ┴
src └───┘└──────────┘└─┘└─────┘┴ ┴ └──────────────────┘┴ └┘
typ └───┘└──────────┘└─┘└─────┘┴┴┴ └──────────────────┘┴┴└┘
doc └───┘ └─┘ ┴ ┴ ┴ └┘
txt └───┘ └─┘ ┴ ┴ ┴ └┘
par └───┘ └─┘ ┴ ┴ ┴ └┘
pid └┘ └─┘ ┴ ┴ ┴ └┘
st ──────────────────────┘└───────────────────────────────────┘└──
588 slice_lhs 1 2 { erw [w (e.inverse.obj j)] }, simp
id ┴ └───────────┘ ┴
src └──────────────┘└───┘ ┴ └───────────┘┴ └─┘┴ └────
typ └──────────────┘└───┘┴┴ └───────────┘┴┴└─┘┴ └────
doc └──────────────┘ ┴ └────
txt └──────────────┘└───┘ ┴ ┴ └─┘┴ └────
par └──────────────┘└───┘ ┴ ┴ └─┘┴ └────
pid ┴└┘└───────┘ ┴ ┴ └──┘ └
st ────────────────────┘└───────────────────────┘ ┴└┘└─────
589 end } }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
590
591 local attribute [elab_simple] inv_fun_id_assoc -- not entirely sure why this is needed
id └──────────────┘
src └──────────────┘
typ └──────────────┘
doc └─────────┘
592 def has_limit_of_equivalence_comp (e : K ≌ J) [has_limit (e.functor ⋙ F)] : has_limit F :=
id ┴ ┴ ┴ └───────┘ ┴└──────┘ ┴ ┴ └───────┘ ┴
src ┴ └───────┘ └──────┘ ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ ┴└──────┘ ┴ ┴ └───────┘ ┴
doc ┴ └───────┘ ┴ └───────┘
593 begin
st └─────
594 haveI : has_limit (e.inverse ⋙ e.functor ⋙ F) := limits.has_limit_equivalence_comp e.symm,
id └───────┘ └───────┘ ┴ └───────┘ ┴ └───────────────────────────────┘ └────┘
src └──────┘└───────┘┴ └───────┘┴┴┴└───────┘┴ ┴ └───┘└───────────────────────────────┘┴└────┘
typ └──────┘└───────┘┴ └───────┘┴┴┴└───────┘┴ ┴┴└───┘└───────────────────────────────┘┴└────┘
doc └──────┘└───────┘┴ ┴┴┴ ┴ ┴ └───┘ ┴
txt └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
par └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
pid ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
595 apply has_limit_of_iso (e.inv_fun_id_assoc F),
id └──────────────┘ └────────────────┘ ┴
src └────┘└──────────────┘┴ └────────────────┘┴ ┴
typ └────┘└──────────────┘┴ └────────────────┘┴┴┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
596 end
st ──┘
597
598 -- `has_limit_comp_equivalence` and `has_limit_of_comp_equivalence`
599 -- are proved in `category_theory/adjunction/limits.lean`.
600
601 section lim_functor
602
603 variables [has_limits_of_shape J C]
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
604
605 /-- `limit F` is functorial in `F`, when `C` has all limits of shape `J`. -/
606 def lim : (J ⥤ C) ⥤ C :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
607 { obj := λ F, limit F,
id ┴ ┴ └───┘ ┴
src ┴ └───┘
typ ┴ ┴ └───┘ ┴
doc ┴
608 map := λ F G α, limit.lift G
id ┴ ┴ ┴ └────────┘ ┴
src └────────┘
typ ┴ ┴ ┴ └────────┘ ┴
609 { X := limit F,
id └───┘ ┴
src └───┘
typ └───┘ ┴
610 π :=
611 { app := λ j, limit.π F j ≫ α.app j,
id ┴ └─────┘ ┴ ┴ ┴ ┴└──┘ ┴
src └─────┘ ┴ └──┘
typ ┴ └─────┘ ┴ ┴ ┴ ┴└──┘ ┴
612 naturality' := λ j j' f,
id ┴ └┘ ┴
typ ┴ └┘ ┴
613 by erw [id_comp, assoc, ←α.naturality, ←assoc, limit.w] } },
id └─────┘ └───┘ └───┘ └─────┘
src └───┘└─────┘└┘└───┘└─┘ └─┘└───┘└┘└─────┘└┘
typ └───┘└─────┘└┘└───┘└─┘└──────────┘└─┘└───┘└┘└─────┘└┘
doc └───┘ └┘ └─┘ └─┘ └┘ └┘
txt └───┘ └┘ └─┘ └─┘ └┘ └┘
par └───┘ └┘ └─┘ └─┘ └┘ └┘
pid └┘ └┘ └─┘ └─┘ └┘ ┴┴
st └───────────┘└─────┘└─────────────┘└──────┘└───────┘┴┴
614 map_comp' := λ F G H α β,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
615 by ext; erw [assoc, is_limit.fac, is_limit.fac, ←assoc, is_limit.fac, assoc]; refl }
id └───┘ └──────────┘ └──────────┘ └───┘ └──────────┘ └───┘
src └─┘ └───┘└───┘└┘ └┘ └─┘└───┘└┘ └┘└───┘┴ └───┘
typ └─┘ └───┘└───┘└┘└──────────┘└┘└──────────┘└─┘└───┘└┘└──────────┘└┘└───┘┴ └───┘
doc └─┘ └───┘ └┘ └┘ └─┘ └┘ └┘ ┴ └───┘
txt └─┘ └───┘ └┘ └┘ └─┘ └┘ └┘ ┴ └───┘
par └─┘ └───┘ └┘ └┘ └─┘ └┘ └┘ ┴ └───┘
pid └┘ └┘ └┘ └─┘ └┘ └┘ ┴ ┴
st └─────────┘└─────────────────────────────────────────────────────────────┘└─────┘
616
617 variables {F} {G : J ⥤ C} (α : F ⟶ G)
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
618
619 @[simp, reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
id ┴ └─┘└──┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴└──┘ ┴
src └─┘└──┘ ┴ └─────┘ ┴ └─────┘ ┴ └──┘
typ ┴ └─┘└──┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴└──┘ ┴
doc └──┘ └─────┘ └─┘
620 by apply is_limit.fac
id └──────────┘
src └────┘ └
typ └────┘└──────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └───────────────────
621
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
622 @[simp] lemma limit.lift_map (c : cone F) :
id └──┘ ┴
src └──┘
typ └──┘ ┴
doc └──┘ └──┘
623 limit.lift F c ≫ lim.map α = limit.lift G ((cones.postcompose α).obj c) :=
id └────────┘ ┴ ┴ ┴ └─┘└──┘ ┴ ┴ └────────┘ ┴ └───────────────┘ ┴ └─┘ ┴
src └────────┘ ┴ └─┘└──┘ ┴ └────────┘ └───────────────┘ └─┘
typ └────────┘ ┴ ┴ ┴ └─┘└──┘ ┴ ┴ └────────┘ ┴ └───────────────┘ ┴ └─┘ ┴
doc └─┘
624 by ext; rw [assoc, lim.map_π, ←assoc, limit.lift_π, limit.lift_π]; refl
id └───┘ └───────┘ └───┘ └──────────┘ └──────────┘
src └─┘ └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘└┘└──────────┘┴ └────
typ └─┘ └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘└┘└──────────┘┴ └────
doc └─┘ └──┘ └┘ └─┘ └┘ └┘ ┴ └────
txt └─┘ └──┘ └┘ └─┘ └┘ └┘ ┴ └────
par └─┘ └──┘ └┘ └─┘ └┘ └┘ ┴ └────
pid └┘ └┘ └─┘ └┘ └┘ ┴ └
st └────────┘└───┘└─────────┘└──────┘└────────────┘└────────────┘┴└──────
625
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
626 lemma limit.map_pre [has_limits_of_shape K C] (E : K ⥤ J) :
id └─────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ ┴
typ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────────┘ ┴
627 lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whisker_left E α) :=
id └─┘└──┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘└──┘ └──────────┘ ┴ ┴
src └─┘└──┘ ┴ └───────┘ ┴ └───────┘ ┴ └─┘└──┘ └──────────┘
typ └─┘└──┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘└──┘ └──────────┘ ┴ ┴
doc └─┘ └─┘
628 by ext; rw [assoc, limit.pre_π, lim.map_π, assoc, lim.map_π, ←assoc, limit.pre_π]; refl
id └───┘ └─────────┘ └───────┘ └───┘ └───────┘ └───┘ └─────────┘
src └─┘ └──┘└───┘└┘└─────────┘└┘└───────┘└┘└───┘└┘└───────┘└─┘└───┘└┘└─────────┘┴ └────
typ └─┘ └──┘└───┘└┘└─────────┘└┘└───────┘└┘└───┘└┘└───────┘└─┘└───┘└┘└─────────┘┴ └────
doc └─┘ └──┘ └┘ └┘ └┘ └┘ └─┘ └┘ ┴ └────
txt └─┘ └──┘ └┘ └┘ └┘ └┘ └─┘ └┘ ┴ └────
par └─┘ └──┘ └┘ └┘ └┘ └┘ └─┘ └┘ ┴ └────
pid └┘ └┘ └┘ └┘ └┘ └─┘ └┘ ┴ └
st └────────┘└───┘└───────────┘└─────────┘└─────┘└─────────┘└──────┘└───────────┘┴└──────
629
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
630 lemma limit.map_pre' [has_limits_of_shape.{v} K C]
id └─────────────────┘ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴
doc └─────────────────┘
631 (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
doc ┴ ┴
632 limit.pre F E₂ = limit.pre F E₁ ≫ lim.map (whisker_right α F) :=
id └───────┘ ┴ └┘ ┴ └───────┘ ┴ └┘ ┴ └─┘└──┘ └───────────┘ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ └─┘└──┘ └───────────┘
typ └───────┘ ┴ └┘ ┴ └───────┘ ┴ └┘ ┴ └─┘└──┘ └───────────┘ ┴ ┴
doc └─┘
633 by ext1; simp [(category.assoc _ _ _ _).symm]
id └────────────┘
src └──┘ └────┘ └────────────┘└───────────────
typ └──┘ └────┘ └────────────┘└───────────────
doc └──┘ └────┘ └───────────────
txt └──┘ └────┘ └───────────────
par └──┘ └────┘ └───────────────
pid ┴┴ └─────────────┘└
st └───────────────────────────────────────────
634
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
635 lemma limit.id_pre (F : J ⥤ C) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
636 limit.pre F (𝟭 _) = lim.map (functor.left_unitor F).inv := by tidy
id └───────┘ ┴ ┴ ┴ └─┘└──┘ └─────────────────┘ ┴ └─┘
src └───────┘ ┴ ┴ └─┘└──┘ └─────────────────┘ └─┘ └────
typ └───────┘ ┴ ┴ ┴ └─┘└──┘ └─────────────────┘ ┴ └─┘ └────
doc ┴ └─┘ └────
txt └────
par └────
pid └
st └─────
637
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
638 lemma limit.map_post {D : Type u'} [category.{v} D] [has_limits_of_shape J D] (H : C ⥤ D) :
id └──────┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ └─────────────────┘ ┴
typ └──────┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └─────────────────┘ ┴
639 /- H (limit F) ⟶ H (limit G) ⟶ limit (G ⋙ H) vs
640 H (limit F) ⟶ limit (F ⋙ H) ⟶ limit (G ⋙ H) -/
641 H.map (lim.map α) ≫ limit.post G H = limit.post F H ≫ lim.map (whisker_right α H) :=
id ┴└──┘ └─┘└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └─┘└──┘ └───────────┘ ┴ ┴
src └──┘ └─┘└──┘ ┴ └────────┘ ┴ └────────┘ ┴ └─┘└──┘ └───────────┘
typ ┴└──┘ └─┘└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └─┘└──┘ └───────────┘ ┴ ┴
doc └─┘ └─┘
642 begin
st └─────
643 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
644 rw [assoc, limit.post_π, ←H.map_comp, lim.map_π, H.map_comp],
id └───┘ └──────────┘ └───────┘
src └──┘└───┘└┘└──────────┘└─┘ └┘└───────┘└┘ ┴
typ └──┘└───┘└┘└──────────┘└─┘└────────┘└┘└───────┘└┘└────────┘┴
doc └──┘ └┘ └─┘ └┘ └┘ ┴
txt └──┘ └┘ └─┘ └┘ └┘ ┴
par └──┘ └┘ └─┘ └┘ └┘ ┴
pid └┘ └┘ └─┘ └┘ └┘ ┴
st ──────────┘└────────────┘└───────────┘└─────────┘└──────────┘└──
645 rw [assoc, lim.map_π, ←assoc, limit.post_π],
id └───┘ └───────┘ └───┘ └──────────┘
src └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘┴
typ └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘┴
doc └──┘ └┘ └─┘ └┘ ┴
txt └──┘ └┘ └─┘ └┘ ┴
par └──┘ └┘ └─┘ └┘ ┴
pid └┘ └┘ └─┘ └┘ ┴
st ──────────┘└─────────┘└──────┘└────────────┘└──
646 refl
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
647 end
st └─┘
648
649 def lim_yoneda : lim ⋙ yoneda ≅ category_theory.cones J C :=
id └─┘ ┴ └────┘ ┴ └───────────────────┘ ┴ ┴
src └─┘ ┴ └────┘ ┴ └───────────────────┘
typ └─┘ ┴ └────┘ ┴ └───────────────────┘ ┴ ┴
doc └─┘ ┴ └───────────────────┘
650 nat_iso.of_components (λ F, nat_iso.of_components (λ W, limit.hom_iso F (unop W)) (by tidy))
id └───────────────────┘ ┴ └───────────────────┘ ┴ └───────────┘ ┴ └──┘ ┴
src └───────────────────┘ └───────────────────┘ └───────────┘ └──┘ └──┘
typ └───────────────────┘ ┴ └───────────────────┘ ┴ └───────────┘ ┴ └──┘ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
651 (by tidy)
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
652
653 end lim_functor
654
655 def has_limits_of_shape_of_equivalence {J' : Type v} [small_category J']
id └────────────┘ └┘
src └────────────┘
typ └────────────┘ └┘
doc └────────────┘
656 (e : J ≌ J') [has_limits_of_shape J C] : has_limits_of_shape J' C :=
id ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └─────────────────┘ └┘ ┴
src ┴ └─────────────────┘ └─────────────────┘
typ ┴ ┴ └┘ └─────────────────┘ ┴ ┴ └─────────────────┘ └┘ ┴
doc ┴ └─────────────────┘ └─────────────────┘
657 by { constructor, intro F, apply has_limit_of_equivalence_comp e, apply_instance }
id └───────────────────────────┘ ┴
src └─────────┘ └─────┘ └────┘└───────────────────────────┘┴ └─────────────┘
typ └─────────┘ └─────┘ └────┘└───────────────────────────┘┴┴ └─────────────┘
doc └─────────┘ └─────┘ └────┘ ┴ └─────────────┘
txt └─────────┘ └─────┘ └────┘ ┴ └─────────────┘
par └─────────┘ └─────┘ └────┘ ┴ └─────────────┘
pid └┘ ┴ ┴ ┴
st └────────────┘└───────┘└─────────────────────────────────────┘└───────────────┘└┘
658
659 end limit
660
661
662 section colimit
663
664 /-- `has_colimit F` represents a particular chosen colimit of the diagram `F`. -/
665 class has_colimit (F : J ⥤ C) :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
666 (cocone : cocone F)
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
667 (is_colimit : is_colimit cocone . tactic.apply_instance)
id └────────┘ └────┘ ┴
src └────────┘
typ └────────┘ └────┘ ┴
doc └────────┘
668
669 variables (J C)
670
671 /-- `C` has colimits of shape `J` if we have chosen a particular colimit of
672 every functor `F : J ⥤ C`. -/
673 class has_colimits_of_shape :=
674 (has_colimit : Π F : J ⥤ C, has_colimit F)
id ┴ ┴ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘
typ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc ┴ └─────────┘
675
676 /-- `C` has all (small) colimits if it has colimits of every shape. -/
677 class has_colimits :=
678 (has_colimits_of_shape : Π (J : Type v) [𝒥 : small_category J], has_colimits_of_shape J C)
id ┴ └──┘ └────────────┘ ┴ └───────────────────┘ ┴ ┴
src └────────────┘ └───────────────────┘
typ ┴ └──┘ └────────────┘ ┴ └───────────────────┘ ┴ ┴
doc └────────────┘ └───────────────────┘
679
680 variables {J C}
681
682 @[priority 100] -- see Note [lower instance priority]
683 instance has_colimit_of_has_colimits_of_shape
684 {J : Type v} [small_category J] [H : has_colimits_of_shape J C] (F : J ⥤ C) : has_colimit F :=
id └────────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴
src └────────────┘ └───────────────────┘ ┴ └─────────┘
typ └────────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc └────────────┘ └───────────────────┘ ┴ └─────────┘
685 has_colimits_of_shape.has_colimit F
id └───────────────────────────────┘ ┴
src └───────────────────────────────┘
typ └───────────────────────────────┘ ┴
686
687 @[priority 100] -- see Note [lower instance priority]
688 instance has_colimits_of_shape_of_has_colimits
689 {J : Type v} [small_category J] [H : has_colimits.{v} C] : has_colimits_of_shape J C :=
id └────────────┘ ┴ └──────────┘ ┴ └───────────────────┘ ┴ ┴
src └────────────┘ └──────────┘ └───────────────────┘
typ └────────────┘ ┴ └──────────┘ ┴ └───────────────────┘ ┴ ┴
doc └────────────┘ └──────────┘ └───────────────────┘
690 has_colimits.has_colimits_of_shape C J
id └────────────────────────────────┘ ┴ ┴
src └────────────────────────────────┘
typ └────────────────────────────────┘ ┴ ┴
691
692 /- Interface to the `has_colimit` class. -/
693
694 def colimit.cocone (F : J ⥤ C) [has_colimit F] : cocone F := has_colimit.cocone F
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ └────────────────┘ ┴
src ┴ └─────────┘ └────┘ └────────────────┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ └────────────────┘ ┴
doc ┴ └─────────┘ └────┘
695
696 def colimit (F : J ⥤ C) [has_colimit F] := (colimit.cocone F).X
id ┴ ┴ ┴ └─────────┘ ┴ └────────────┘ ┴ ┴
src ┴ └─────────┘ └────────────┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ └────────────┘ ┴ ┴
doc ┴ └─────────┘
697
698 def colimit.ι (F : J ⥤ C) [has_colimit F] (j : J) : F.obj j ⟶ colimit F :=
id ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴└──┘ ┴ ┴ └─────┘ ┴
src ┴ └─────────┘ └──┘ ┴ └─────┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴└──┘ ┴ ┴ └─────┘ ┴
doc ┴ └─────────┘
699 (colimit.cocone F).ι.app j
id └────────────┘ ┴ ┴ └─┘ ┴
src └────────────┘ ┴ └─┘
typ └────────────┘ ┴ ┴ └─┘ ┴
700
701 @[simp] lemma colimit.cocone_ι {F : J ⥤ C} [has_colimit F] (j : J) :
id ┴ ┴ ┴ └─────────┘ ┴ ┴
src ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └──┘ ┴ └─────────┘
702 (colimit.cocone F).ι.app j = colimit.ι _ j := rfl
id └────────────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘ ┴ └─┘
src └────────────┘ ┴ └─┘ ┴ └───────┘ └─┘
typ └────────────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘ ┴ └─┘
703
704 @[simp] lemma colimit.w (F : J ⥤ C) [has_colimit F] {j j' : J} (f : j ⟶ j') :
id ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └┘
src ┴ └─────────┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └┘
doc └──┘ ┴ └─────────┘
705 F.map f ≫ colimit.ι F j' = colimit.ι F j := (colimit.cocone F).w f
id ┴└──┘ ┴ ┴ └───────┘ ┴ └┘ ┴ └───────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
src └──┘ ┴ └───────┘ ┴ └───────┘ └────────────┘ ┴
typ ┴└──┘ ┴ ┴ └───────┘ ┴ └┘ ┴ └───────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
706
707 def colimit.is_colimit (F : J ⥤ C) [has_colimit F] : is_colimit (colimit.cocone F) :=
id ┴ ┴ ┴ └─────────┘ ┴ └────────┘ └────────────┘ ┴
src ┴ └─────────┘ └────────┘ └────────────┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────────┘ └────────────┘ ┴
doc ┴ └─────────┘ └────────┘
708 has_colimit.is_colimit.{v} F
id └────────────────────┘ ┴
src └────────────────────┘
typ └────────────────────┘ ┴
709
710 def colimit.desc (F : J ⥤ C) [has_colimit F] (c : cocone F) : colimit F ⟶ c.X :=
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴└┘
src ┴ └─────────┘ └────┘ └─────┘ ┴ └┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴└┘
doc ┴ └─────────┘ └────┘
711 (colimit.is_colimit F).desc c
id └────────────────┘ ┴ └──┘ ┴
src └────────────────┘ └──┘
typ └────────────────┘ ┴ └──┘ ┴
712
713 @[simp] lemma colimit.is_colimit_desc {F : J ⥤ C} [has_colimit F] (c : cocone F) :
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴
src ┴ └─────────┘ └────┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴
doc └──┘ ┴ └─────────┘ └────┘
714 (colimit.is_colimit F).desc c = colimit.desc F c := rfl
id └────────────────┘ ┴ └──┘ ┴ ┴ └──────────┘ ┴ ┴ └─┘
src └────────────────┘ └──┘ ┴ └──────────┘ └─┘
typ └────────────────┘ ┴ └──┘ ┴ ┴ └──────────┘ ┴ ┴ └─┘
715
716 /--
717 We have lots of lemmas describing how to simplify `colimit.ι F j ≫ _`,
718 and combined with `colimit.ext` we rely on these lemmas for many calculations.
719
720 However, since `category.assoc` is a `@[simp]` lemma, often expressions are
721 right associated, and it's hard to apply these lemmas about `colimit.ι`.
722
723 We thus use `reassoc` to define additional `@[simp]` lemmas, with an arbitrary extra morphism.
724 (see `tactic/reassoc_axiom.lean`)
725 -/
726 @[simp, reassoc] lemma colimit.ι_desc {F : J ⥤ C} [has_colimit F] (c : cocone F) (j : J) :
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴
src ┴ └─────────┘ └────┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴
doc └──┘ └─────┘ ┴ └─────────┘ └────┘
727 colimit.ι F j ≫ colimit.desc F c = c.ι.app j :=
id └───────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└┘└──┘ ┴
src └───────┘ ┴ └──────────┘ ┴ └┘└──┘
typ └───────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└┘└──┘ ┴
728 is_colimit.fac _ c j
id └────────────┘ ┴ ┴
typ └────────────┘ ┴ ┴
729
730 def colimit.cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) :
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴
src ┴ └─────────┘ └────┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴
doc ┴ └─────────┘ └────┘
731 cocone_morphism (colimit.cocone F) c :=
id └─────────────┘ └────────────┘ ┴ ┴
src └─────────────┘ └────────────┘
typ └─────────────┘ └────────────┘ ┴ ┴
732 (colimit.is_colimit F).desc_cocone_morphism c
id └────────────────┘ ┴ └──────────────────┘ ┴
src └────────────────┘ └──────────────────┘
typ └────────────────┘ ┴ └──────────────────┘ ┴
733
734 @[simp] lemma colimit.cocone_morphism_hom {F : J ⥤ C} [has_colimit F] (c : cocone F) :
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴
src ┴ └─────────┘ └────┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴
doc └──┘ ┴ └─────────┘ └────┘
735 (colimit.cocone_morphism c).hom = colimit.desc F c := rfl
id └─────────────────────┘ ┴ └─┘ ┴ └──────────┘ ┴ ┴ └─┘
src └─────────────────────┘ └─┘ ┴ └──────────┘ └─┘
typ └─────────────────────┘ ┴ └─┘ ┴ └──────────┘ ┴ ┴ └─┘
736 @[simp] lemma colimit.ι_cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) (j : J) :
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴
src ┴ └─────────┘ └────┘
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴
doc └──┘ ┴ └─────────┘ └────┘
737 colimit.ι F j ≫ (colimit.cocone_morphism c).hom = c.ι.app j :=
id └───────┘ ┴ ┴ ┴ └─────────────────────┘ ┴ └─┘ ┴ ┴└┘└──┘ ┴
src └───────┘ ┴ └─────────────────────┘ └─┘ ┴ └┘└──┘
typ └───────┘ ┴ ┴ ┴ └─────────────────────┘ ┴ └─┘ ┴ ┴└┘└──┘ ┴
738 by erw is_colimit.fac
id └────────────┘
src └──┘ └
typ └──┘└────────────┘└
doc └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └───────────────────
739
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
740 @[ext] lemma colimit.hom_ext {F : J ⥤ C} [has_colimit F] {X : C} {f f' : colimit F ⟶ X}
id ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src ┴ └─────────┘ └─────┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─┘ ┴ └─────────┘
741 (w : ∀ j, colimit.ι F j ≫ f = colimit.ι F j ≫ f') : f = f' :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
src └───────┘ ┴ ┴ └───────┘ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
742 (colimit.is_colimit F).hom_ext w
id └────────────────┘ ┴ └─────┘ ┴
src └────────────────┘ └─────┘
typ └────────────────┘ ┴ └─────┘ ┴
doc └─────┘
743
744 def colimit.hom_iso (F : J ⥤ C) [has_colimit F] (W : C) : (colimit F ⟶ W) ≅ (F.cocones.obj W) :=
id ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└──────┘└──┘ ┴
src ┴ └─────────┘ └─────┘ ┴ ┴ └──────┘└──┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└──────┘└──┘ ┴
doc ┴ └─────────┘ └──────┘
745 (colimit.is_colimit F).hom_iso W
id └────────────────┘ ┴ └─────┘ ┴
src └────────────────┘ └─────┘
typ └────────────────┘ ┴ └─────┘ ┴
doc └─────┘
746
747 @[simp] lemma colimit.hom_iso_hom (F : J ⥤ C) [has_colimit F] {W : C} (f : colimit F ⟶ W) :
id ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src ┴ └─────────┘ └─────┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └──┘ ┴ └─────────┘
748 (colimit.hom_iso F W).hom f = (colimit.cocone F).ι ≫ (const J).map f :=
id └─────────────┘ ┴ ┴ └─┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴
src └─────────────┘ └─┘ ┴ └────────────┘ ┴ ┴ └───┘ └─┘
typ └─────────────┘ ┴ ┴ └─┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └───┘ ┴ └─┘ ┴
749 (colimit.is_colimit F).hom_iso_hom f
id └────────────────┘ ┴ └─────────┘ ┴
src └────────────────┘ └─────────┘
typ └────────────────┘ ┴ └─────────┘ ┴
750
751 def colimit.hom_iso' (F : J ⥤ C) [has_colimit F] (W : C) :
id ┴ ┴ ┴ └─────────┘ ┴ ┴
src ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc ┴ └─────────┘
752 ((colimit F ⟶ W) : Type v) ≅ { p : Π j, F.obj j ⟶ W // ∀ {j j'} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴└──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
753 (colimit.is_colimit F).hom_iso' W
id └────────────────┘ ┴ └──────┘ ┴
src └────────────────┘ └──────┘
typ └────────────────┘ ┴ └──────┘ ┴
754
755 lemma colimit.desc_extend (F : J ⥤ C) [has_colimit F] (c : cocone F) {X : C} (f : c.X ⟶ X) :
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴ ┴└┘ ┴ ┴
src ┴ └─────────┘ └────┘ └┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴ ┴└┘ ┴ ┴
doc ┴ └─────────┘ └────┘
756 colimit.desc F (c.extend f) = colimit.desc F c ≫ f :=
id └──────────┘ ┴ ┴└─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └─────┘ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴└─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └─────┘
757 begin
st └─────
758 ext1, rw [←category.assoc], simp
id └────────────┘
src └──┘ └───┘└────────────┘┴ └───┘
typ └──┘ └───┘└────────────┘┴ └───┘
doc └──┘ └───┘ ┴ └───┘
txt └──┘ └───┘ ┴ └───┘
par └──┘ └───┘ ┴ └───┘
pid └─┘ ┴ ┴
st ─────┘└───────────────────┘└──────┘
759 end
st └─┘
760
761 def has_colimit_of_iso {F G : J ⥤ C} [has_colimit F] (α : G ≅ F) : has_colimit G :=
id ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘ ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc ┴ └─────────┘ └─────────┘
762 { cocone := (cocones.precompose α.hom).obj (colimit.cocone F),
id └────────────────┘ ┴└──┘ └─┘ └────────────┘ ┴
src └────────────────┘ └──┘ └─┘ └────────────┘
typ └────────────────┘ ┴└──┘ └─┘ └────────────┘ ┴
763 is_colimit :=
764 { desc := λ s, colimit.desc F ((cocones.precompose α.inv).obj s),
id ┴ └──────────┘ ┴ └────────────────┘ ┴└──┘ └─┘ ┴
src └──────────┘ └────────────────┘ └──┘ └─┘
typ ┴ └──────────┘ ┴ └────────────────┘ ┴└──┘ └─┘ ┴
765 fac' := λ s j,
id ┴ ┴
typ ┴ ┴
766 begin
st └─────
767 rw [cocones.precompose_obj_ι, nat_trans.comp_app, colimit.cocone_ι],
id └──────────────────────┘ └────────────────┘ └──────────────┘
src └──┘└──────────────────────┘└┘└────────────────┘└┘└──────────────┘┴
typ └──┘└──────────────────────┘└┘└────────────────┘└┘└──────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ─────────────────────────────────┘└──────────────────┘└────────────────┘└──
768 rw [category.assoc, colimit.ι_desc, ←nat_iso.app_hom, ←iso.eq_inv_comp], refl
id └────────────┘ └────────────┘ └─────────────┘ └─────────────┘
src └──┘└────────────┘└┘└────────────┘└─┘└─────────────┘└─┘└─────────────┘┴ └────
typ └──┘└────────────┘└┘└────────────┘└─┘└─────────────┘└─┘└─────────────┘┴ └────
doc └──┘ └┘└────────────┘└─┘ └─┘ ┴ └────
txt └──┘ └┘ └─┘ └─┘ ┴ └────
par └──┘ └┘ └─┘ └─┘ ┴ └────
pid └┘ └┘ └─┘ └─┘ ┴ └
st ───────────────────────┘└──────────────┘└────────────────┘└────────────────┘└───────
769 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
770 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
771 begin
st └─────
772 apply colimit.hom_ext, intro j,
id └─────────────┘
src └────┘└─────────────┘ └─────┘
typ └────┘└─────────────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ──────────────────────────┘└───────┘└─
773 rw [colimit.ι_desc, cocones.precompose_obj_ι, nat_trans.comp_app, ←nat_iso.app_inv,
id └────────────┘ └──────────────────────┘ └────────────────┘ └─────────────┘
src └──┘└────────────┘└┘└──────────────────────┘└┘└────────────────┘└─┘└─────────────┘└─
typ └──┘└────────────┘└┘└──────────────────────┘└┘└────────────────┘└─┘└─────────────┘└─
doc └──┘└────────────┘└┘ └┘ └─┘ └─
txt └──┘ └┘ └┘ └─┘ └─
par └──┘ └┘ └┘ └─┘ └─
pid └┘ └┘ └┘ └─┘ └─
st ───────────────────────┘└────────────────────────┘└──────────────────┘└────────────────┘└─
774 iso.eq_inv_comp],
id └─────────────┘
src ───────┘└─────────────┘┴
typ ───────┘└─────────────┘┴
doc ───────┘ ┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ──────────────────────┘└──
775 simpa using w j
id ┴ ┴
src └──────────┘ ┴ └
typ └──────────┘┴┴┴└
doc └──────────┘ ┴ └
txt └──────────┘ ┴ └
par └──────────┘ ┴ └
pid ┴└────┘ ┴ └
st ──────────────────────
776 end } }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
777
778 /-- If a functor `G` has the same collection of cocones as a functor `F`
779 which has a colimit, then `G` also has a colimit. -/
780 def has_colimit.of_cocones_iso {J K : Type v} [small_category J] [small_category K] (F : J ⥤ C) (G : K ⥤ C)
id └────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └────────────┘ ┴ ┴
typ └────────────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────┘ └────────────┘ ┴ ┴
781 (h : F.cocones ≅ G.cocones) [has_colimit F] : has_colimit G :=
id ┴└──────┘ ┴ ┴└──────┘ └─────────┘ ┴ └─────────┘ ┴
src └──────┘ ┴ └──────┘ └─────────┘ └─────────┘
typ ┴└──────┘ ┴ ┴└──────┘ └─────────┘ ┴ └─────────┘ ┴
doc └──────┘ └──────┘ └─────────┘ └─────────┘
782 ⟨_, is_colimit.of_nat_iso ((is_colimit.nat_iso (colimit.is_colimit F)) ≪≫ h)⟩
id └───────────────────┘ └────────────────┘ └────────────────┘ ┴ └┘ ┴
src └───────────────────┘ └────────────────┘ └────────────────┘ └┘
typ └───────────────────┘ └────────────────┘ └────────────────┘ ┴ └┘ ┴
doc └───────────────────┘ └────────────────┘
783
784 section pre
785 variables (F) [has_colimit F] (E : K ⥤ J) [has_colimit (E ⋙ F)]
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ ┴ └─────────┘ ┴
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ ┴ └─────────┘ ┴
786
787 def colimit.pre : colimit (E ⋙ F) ⟶ colimit F :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc ┴
788 colimit.desc (E ⋙ F)
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc ┴
789 { X := colimit F,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
790 ι := { app := λ k, colimit.ι F (E.obj k) } }
id ┴ ┴ └───────┘ ┴ ┴└──┘ ┴
src ┴ └───────┘ └──┘
typ ┴ ┴ └───────┘ ┴ ┴└──┘ ┴
doc ┴
791
792 @[simp, reassoc] lemma colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴└──┘ ┴
src └───────┘ ┴ ┴ └─────────┘ ┴ └───────┘ └──┘
typ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴└──┘ ┴
doc └──┘ └─────┘ ┴
793 by erw is_colimit.fac
id └────────────┘
src └──┘ └
typ └──┘└────────────┘└
doc └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └───────────────────
794
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
795 @[simp] lemma colimit.pre_desc (c : cocone F) :
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └──┘ └────┘
796 colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) :=
id └─────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└──────┘ ┴
src └─────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ └──────┘
typ └─────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└──────┘ ┴
doc ┴
797 by ext; rw [←assoc, colimit.ι_pre]; simp
id └───┘ └───────────┘
src └─┘ └───┘└───┘└┘└───────────┘┴ └────
typ └─┘ └───┘└───┘└┘└───────────┘┴ └────
doc └─┘ └───┘ └┘ ┴ └────
txt └─┘ └───┘ └┘ ┴ └────
par └─┘ └───┘ └┘ ┴ └────
pid └─┘ └┘ ┴ └
st └────────┘└────┘└─────────────┘┴└──────
798
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
799 variables {L : Type v} [small_category L]
id └────────────┘
src └────────────┘
typ └────────────┘
doc └────────────┘
800 variables (D : L ⥤ K) [has_colimit (D ⋙ E ⋙ F)]
id ┴ └─────────┘ ┴ ┴
src ┴ └─────────┘ ┴ ┴
typ ┴ └─────────┘ ┴ ┴
doc ┴ └─────────┘ ┴ ┴
801
802 @[simp] lemma colimit.pre_pre : colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E) :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴
doc └──┘ ┴ ┴
803 begin
st └─────
804 ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
805 rw [←assoc, colimit.ι_pre, colimit.ι_pre],
id └───┘ └───────────┘ └───────────┘
src └───┘└───┘└┘└───────────┘└┘└───────────┘┴
typ └───┘└───┘└┘└───────────┘└┘└───────────┘┴
doc └───┘ └┘ └┘ ┴
txt └───┘ └┘ └┘ ┴
par └───┘ └┘ └┘ ┴
pid └─┘ └┘ └┘ ┴
st ───────────┘└─────────────┘└─────────────┘└──
806 letI : has_colimit ((D ⋙ E) ⋙ F) := show has_colimit (D ⋙ E ⋙ F), by apply_instance,
id └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └─────┘└─────────┘┴ ┴┴┴ └┘ ┴ └───┘ ┴└─────────┘┴ ┴ ┴ ┴ ┴ └────┘└────────────┘
typ └─────┘└─────────┘┴ ┴┴┴┴┴└┘ ┴┴└───┘ ┴└─────────┘┴ ┴┴ ┴┴┴ ┴┴└────┘└────────────┘
doc └─────┘└─────────┘┴ ┴┴┴ └┘ ┴ └───┘ ┴└─────────┘┴ ┴ ┴ ┴ ┴ └────┘└────────────┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└────────────┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└────────────┘
pid ┴└┘ ┴ ┴ ┴ └┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────────┘
st ─────────────────────────────────────────────────────────────────────┘└─────────────┘└─
807 exact (colimit.ι_pre F (D ⋙ E) j).symm
id └───────────┘ ┴ ┴ ┴ ┴
src └────┘ └───────────┘┴ ┴ ┴ ┴ └┘ └─────┘
typ └────┘ └───────────┘┴┴┴ ┴┴ ┴┴└┘┴└─────┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ └─────┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ └─────┘
par └────┘ ┴ ┴ ┴ ┴ └┘ └─────┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └───┘└┘
st ────────────────────────────────────────┘
808 end
st └─┘
809
810 end pre
811
812 section post
813 variables {D : Type u'} [𝒟 : category.{v} D]
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
814 include 𝒟
815
816 variables (F) [has_colimit F] (G : C ⥤ D) [has_colimit (F ⋙ G)]
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ ┴ └─────────┘ ┴
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ ┴ └─────────┘ ┴
817
818 def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴└──┘ └─────┘ ┴
src └─────┘ ┴ ┴ └──┘ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴└──┘ └─────┘ ┴
doc ┴
819 colimit.desc (F ⋙ G)
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc ┴
820 { X := G.obj (colimit F),
id ┴└──┘ └─────┘ ┴
src └──┘ └─────┘
typ ┴└──┘ └─────┘ ┴
821 ι :=
822 { app := λ j, G.map (colimit.ι F j),
id ┴ ┴└──┘ └───────┘ ┴ ┴
src └──┘ └───────┘
typ ┴ ┴└──┘ └───────┘ ┴ ┴
823 naturality' :=
824 by intros j j' f; erw [←G.map_comp, limits.cocone.w, comp_id]; refl } }
id └─────────────┘ └─────┘
src └───────────┘ └────┘ └┘└─────────────┘└┘└─────┘┴ └───┘
typ └───────────┘ └────┘└────────┘└┘└─────────────┘└┘└─────┘┴ └───┘
doc └───────────┘ └────┘ └┘ └┘ ┴ └───┘
txt └───────────┘ └────┘ └┘ └┘ ┴ └───┘
par └───────────┘ └────┘ └┘ └┘ ┴ └───┘
pid └─────┘ └─┘ └┘ └┘ ┴ ┴
st └───────────────────┘└─────────┘└───────────────┘└───────┘┴└─────┘
825
826 @[simp, reassoc] lemma colimit.ι_post (j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G = G.map (colimit.ι F j) :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└──┘ └───────┘ ┴ ┴
src └───────┘ ┴ ┴ └──────────┘ ┴ └──┘ └───────┘
typ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└──┘ └───────┘ ┴ ┴
doc └──┘ └─────┘ ┴
827 by erw is_colimit.fac
id └────────────┘
src └──┘ └
typ └──┘└────────────┘└
doc └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └───────────────────
828
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
829 @[simp] lemma colimit.post_desc (c : cocone F) :
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └──┘ └────┘
830 colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.map_cocone c) :=
id └──────────┘ ┴ ┴ ┴ ┴└──┘ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└─────────┘ ┴
src └──────────┘ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴ └─────────┘
typ └──────────┘ ┴ ┴ ┴ ┴└──┘ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴└─────────┘ ┴
doc ┴ └─────────┘
831 by ext; rw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_desc, colimit.ι_desc]; refl
id └───┘ └────────────┘ └────────────┘ └────────────┘
src └─┘ └───┘└───┘└┘└────────────┘└─┘ └┘└────────────┘└┘└────────────┘┴ └────
typ └─┘ └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└────────────┘└┘└────────────┘┴ └────
doc └─┘ └───┘ └┘ └─┘ └┘└────────────┘└┘└────────────┘┴ └────
txt └─┘ └───┘ └┘ └─┘ └┘ └┘ ┴ └────
par └─┘ └───┘ └┘ └─┘ └┘ └┘ ┴ └────
pid └─┘ └┘ └─┘ └┘ └┘ ┴ └
st └────────┘└────┘└──────────────┘└───────────┘└──────────────┘└──────────────┘┴└──────
832
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
833 @[simp] lemma colimit.post_post
doc └──┘
834 {E : Type u''} [category.{v} E] (H : D ⥤ E) [has_colimit ((F ⋙ G) ⋙ H)] :
id └──────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─────────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ ┴ └─────────┘ ┴ ┴
835 /- H G (colimit F) ⟶ H (colimit (F ⋙ G)) ⟶ colimit ((F ⋙ G) ⋙ H) equals -/
836 /- H G (colimit F) ⟶ colimit (F ⋙ (G ⋙ H)) -/
837 colimit.post (F ⋙ G) H ≫ H.map (colimit.post F G) = colimit.post F (G ⋙ H) :=
id └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc ┴ ┴
838 begin
st └─────
839 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
840 rw [←assoc, colimit.ι_post, ←H.map_comp, colimit.ι_post],
id └───┘ └────────────┘ └────────────┘
src └───┘└───┘└┘└────────────┘└─┘ └┘└────────────┘┴
typ └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└────────────┘┴
doc └───┘ └┘ └─┘ └┘ ┴
txt └───┘ └┘ └─┘ └┘ ┴
par └───┘ └┘ └─┘ └┘ ┴
pid └─┘ └┘ └─┘ └┘ ┴
st ───────────┘└──────────────┘└───────────┘└──────────────┘└──
841 exact (colimit.ι_post F (G ⋙ H) j).symm
id └────────────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └────────────┘┴ ┴ ┴┴┴ └┘ └─────┘
typ └────┘ └────────────┘┴┴┴ ┴┴┴┴┴└┘┴└─────┘
doc └────┘ ┴ ┴ ┴┴┴ └┘ └─────┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ └─────┘
par └────┘ ┴ ┴ ┴ ┴ └┘ └─────┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └───┘└┘
st ─────────────────────────────────────────┘
842 end
st └─┘
843
844 end post
845
846 lemma colimit.pre_post {D : Type u'} [category.{v} D]
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
847 (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴
848 [has_colimit F] [has_colimit (E ⋙ F)] [has_colimit (F ⋙ G)] [has_colimit ((E ⋙ F) ⋙ G)] :
id └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴
typ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴
849 /- G (colimit F) ⟶ G (colimit (E ⋙ F)) ⟶ colimit ((E ⋙ F) ⋙ G) vs -/
850 /- G (colimit F) ⟶ colimit F ⋙ G ⟶ colimit (E ⋙ (F ⋙ G)) or -/
851 colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G :=
id └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ ┴ ┴ └──┘ └─────────┘ ┴ └─────────┘ ┴ ┴ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ └─────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴
doc ┴ ┴
852 begin
st └─────
853 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
854 rw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_pre, ←assoc],
id └───┘ └────────────┘ └───────────┘ └───┘
src └───┘└───┘└┘└────────────┘└─┘ └┘└───────────┘└─┘└───┘┴
typ └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└───────────┘└─┘└───┘┴
doc └───┘ └┘ └─┘ └┘ └─┘ ┴
txt └───┘ └┘ └─┘ └┘ └─┘ ┴
par └───┘ └┘ └─┘ └┘ └─┘ ┴
pid └─┘ └┘ └─┘ └┘ └─┘ ┴
st ───────────┘└──────────────┘└───────────┘└─────────────┘└──────┘└──
855 letI : has_colimit (E ⋙ F ⋙ G) := show has_colimit ((E ⋙ F) ⋙ G), by apply_instance,
id └─────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └─────┘└─────────┘┴ ┴┴┴ ┴ ┴ └───┘ ┴└─────────┘┴ ┴ ┴ └┘ ┴ └────┘└────────────┘
typ └─────┘└─────────┘┴ ┴┴┴┴┴┴ ┴┴└───┘ ┴└─────────┘┴ ┴┴ ┴┴└┘ ┴┴└────┘└────────────┘
doc └─────┘└─────────┘┴ ┴┴┴ ┴ ┴ └───┘ ┴└─────────┘┴ ┴ ┴ └┘ ┴ └────┘└────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └────┘└────────────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ └────┘└────────────┘
pid ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └┘ ┴ └──────────────────┘
st ─────────────────────────────────────────────────────────────────────┘└─────────────┘└─
856 erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]
id └───────────┘ ┴ ┴ ┴ ┴ └────────────┘
src └───┘└───────────┘┴ ┴ ┴ └┘ ┴ └┘└────────────┘└┘
typ └───┘└───────────┘┴ ┴┴ ┴┴└┘┴┴┴└┘└────────────┘└┘
doc └───┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
txt └───┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
par └───┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘
pid └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴┴
st ───────────────────────────────┘└──────────────┘┴┴
857 end
st └─┘
858
859 open category_theory.equivalence
860 instance has_colimit_equivalence_comp (e : K ≌ J) [has_colimit F] : has_colimit (e.functor ⋙ F) :=
id ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴└──────┘ ┴ ┴
src ┴ └─────────┘ └─────────┘ └──────┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ └─────────┘ ┴└──────┘ ┴ ┴
doc ┴ └─────────┘ └─────────┘ ┴
861 { cocone := cocone.whisker e.functor (colimit.cocone F),
id └────────────┘ ┴└──────┘ └────────────┘ ┴
src └────────────┘ └──────┘ └────────────┘
typ └────────────┘ ┴└──────┘ └────────────┘ ┴
862 is_colimit := let e' := cocones.precompose (e.inv_fun_id_assoc F).inv in
id └┘ └────────────────┘ ┴└───────────────┘ ┴ └─┘
src └────────────────┘ └───────────────┘ └─┘
typ └┘ └────────────────┘ ┴└───────────────┘ ┴ └─┘
863 { desc := λ s, colimit.desc F (e'.obj (cocone.whisker e.inverse s)),
id ┴ └──────────┘ ┴ └┘└──┘ └────────────┘ ┴└──────┘ ┴
src └──────────┘ └──┘ └────────────┘ └──────┘
typ ┴ └──────────┘ ┴ └┘└──┘ └────────────┘ ┴└──────┘ ┴
864 fac' := λ s j,
id ┴ ┴
typ ┴ ┴
865 begin
st └─────
866 dsimp, rw [colimit.ι_desc], dsimp [e'],
id └────────────┘ └┘
src └───┘ └──┘└────────────┘┴ └─────┘ ┴
typ └───┘ └──┘└────────────┘┴ └─────┘└┘┴
doc └───┘ └──┘└────────────┘┴ └─────┘ ┴
txt └───┘ └──┘ ┴ └─────┘ ┴
par └───┘ └──┘ ┴ └─────┘ ┴
pid └┘ ┴ ┴┴ ┴
st ──────────┘└──────────────────┘└───────────┘└─
867 erw [inv_fun_id_assoc_inv_app, ←functor_unit, s.ι.naturality, comp_id], refl
id └──────────────────────┘ └──────────┘ └─────┘
src └───┘└──────────────────────┘└─┘└──────────┘└┘ └┘└─────┘┴ └────
typ └───┘└──────────────────────┘└─┘└──────────┘└┘└────────────┘└┘└─────┘┴ └────
doc └───┘ └─┘ └┘ └┘ ┴ └────
txt └───┘ └─┘ └┘ └┘ ┴ └────
par └───┘ └─┘ └┘ └┘ ┴ └────
pid └┘ └─┘ └┘ └┘ ┴ └
st ──────────────────────────────────┘└─────────────┘└──────────────┘└───────┘└───────
868 end,
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
869 uniq' := λ s m w,
id ┴ ┴ ┴
typ ┴ ┴ ┴
870 begin
st └─────
871 apply colimit.hom_ext, intro j,
id └─────────────┘
src └────┘└─────────────┘ └─────┘
typ └────┘└─────────────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ──────────────────────────┘└───────┘└─
872 erw [colimit.ι_desc],
id └────────────┘
src └───┘└────────────┘┴
typ └───┘└────────────┘┴
doc └───┘└────────────┘┴
txt └───┘ ┴
par └───┘ ┴
pid └┘ ┴
st ────────────────────────┘└──
873 have := w (e.inverse.obj j), simp at this, erw [←colimit.w F (e.counit_iso.hom.app j)] at this,
id ┴ └───────────┘ ┴ └───────┘ ┴ └──────────────────┘ ┴
src └──────┘ ┴ └───────────┘┴ ┴ └──────────┘ └────┘└───────┘┴ ┴ └──────────────────┘┴ └────────┘
typ └──────┘┴┴ └───────────┘┴┴┴ └──────────┘ └────┘└───────┘┴┴┴ └──────────────────┘┴┴└────────┘
doc └──────┘ ┴ ┴ ┴ └──────────┘ └────┘ ┴ ┴ ┴ └────────┘
txt └──────┘ ┴ ┴ ┴ └──────────┘ └────┘ ┴ ┴ ┴ └────────┘
par └──────┘ ┴ ┴ ┴ └──────────┘ └────┘ ┴ ┴ ┴ └────────┘
pid └───┘└─┘ ┴ ┴ ┴ ┴└─────┘ └─┘ ┴ ┴ ┴ └┘└──────┘
st ────────────────────────────────┘└────────────┘└──────────────────────────────────────────┘┴└──────┘└─
874 erw [assoc, ←iso.eq_inv_comp (F.map_iso $ e.counit_iso.app j)] at this, erw [this], simp
id └───┘ └─────────────┘ └───────┘ └──────────────┘ ┴ └──┘
src └───┘└───┘└─┘└─────────────┘┴ └───────┘┴ ┴└──────────────┘┴ └────────┘ └───┘ ┴ └────
typ └───┘└───┘└─┘└─────────────┘┴ └───────┘┴ ┴└──────────────┘┴┴└────────┘ └───┘└──┘┴ └────
doc └───┘ └─┘ ┴ ┴ ┴└──────────────┘┴ └────────┘ └───┘ ┴ └────
txt └───┘ └─┘ ┴ ┴ ┴ ┴ └────────┘ └───┘ ┴ └────
par └───┘ └─┘ ┴ ┴ ┴ ┴ └────────┘ └───┘ ┴ └────
pid └┘ └─┘ ┴ ┴ ┴ ┴ └┘└──────┘ └┘ ┴ └
st ───────────────┘└─────────────────────────────────────────────────┘┴└──────┘└─────────┘└───────
875 end } }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
876
877 def has_colimit_of_equivalence_comp (e : K ≌ J) [has_colimit (e.functor ⋙ F)] : has_colimit F :=
id ┴ ┴ ┴ └─────────┘ ┴└──────┘ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘ └──────┘ ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘ ┴└──────┘ ┴ ┴ └─────────┘ ┴
doc ┴ └─────────┘ ┴ └─────────┘
878 begin
st └─────
879 haveI : has_colimit (e.inverse ⋙ e.functor ⋙ F) := limits.has_colimit_equivalence_comp e.symm,
id └─────────┘ └───────┘ ┴ └───────┘ ┴ └─────────────────────────────────┘ └────┘
src └──────┘└─────────┘┴ └───────┘┴┴┴└───────┘┴ ┴ └───┘└─────────────────────────────────┘┴└────┘
typ └──────┘└─────────┘┴ └───────┘┴┴┴└───────┘┴ ┴┴└───┘└─────────────────────────────────┘┴└────┘
doc └──────┘└─────────┘┴ ┴┴┴ ┴ ┴ └───┘ ┴
txt └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
par └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
pid ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
880 apply has_colimit_of_iso (e.inv_fun_id_assoc F).symm,
id └────────────────┘ └────────────────┘ ┴
src └────┘└────────────────┘┴ └────────────────┘┴ └────┘
typ └────┘└────────────────┘┴ └────────────────┘┴┴└────┘
doc └────┘ ┴ ┴ └────┘
txt └────┘ ┴ ┴ └────┘
par └────┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ └───┘┴
st ─────────────────────────────────────────────────────┘└─
881 end
st ──┘
882
883 section colim_functor
884
885 variables [has_colimits_of_shape J C]
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
886
887 /-- `colimit F` is functorial in `F`, when `C` has all colimits of shape `J`. -/
888 def colim : (J ⥤ C) ⥤ C :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
889 { obj := λ F, colimit F,
id ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴
doc ┴
890 map := λ F G α, colimit.desc F
id ┴ ┴ ┴ └──────────┘ ┴
src └──────────┘
typ ┴ ┴ ┴ └──────────┘ ┴
891 { X := colimit G,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
892 ι :=
893 { app := λ j, α.app j ≫ colimit.ι G j,
id ┴ ┴└──┘ ┴ ┴ └───────┘ ┴ ┴
src └──┘ ┴ └───────┘
typ ┴ ┴└──┘ ┴ ┴ └───────┘ ┴ ┴
894 naturality' := λ j j' f,
id ┴ └┘ ┴
typ ┴ └┘ ┴
895 by erw [comp_id, ←assoc, α.naturality, assoc, colimit.w] } },
id └─────┘ └───┘ └───┘ └───────┘
src └───┘└─────┘└─┘└───┘└┘ └┘└───┘└┘└───────┘└┘
typ └───┘└─────┘└─┘└───┘└┘└──────────┘└┘└───┘└┘└───────┘└┘
doc └───┘ └─┘ └┘ └┘ └┘ └┘
txt └───┘ └─┘ └┘ └┘ └┘ └┘
par └───┘ └─┘ └┘ └┘ └┘ └┘
pid └┘ └─┘ └┘ └┘ └┘ ┴┴
st └───────────┘└──────┘└────────────┘└─────┘└─────────┘┴┴
896 map_comp' := λ F G H α β,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
897 by ext; erw [←assoc, is_colimit.fac, is_colimit.fac, assoc, is_colimit.fac, ←assoc]; refl }
id └───┘ └────────────┘ └────────────┘ └───┘ └────────────┘ └───┘
src └─┘ └────┘└───┘└┘ └┘ └┘└───┘└┘ └─┘└───┘┴ └───┘
typ └─┘ └────┘└───┘└┘└────────────┘└┘└────────────┘└┘└───┘└┘└────────────┘└─┘└───┘┴ └───┘
doc └─┘ └────┘ └┘ └┘ └┘ └┘ └─┘ ┴ └───┘
txt └─┘ └────┘ └┘ └┘ └┘ └┘ └─┘ ┴ └───┘
par └─┘ └────┘ └┘ └┘ └┘ └┘ └─┘ ┴ └───┘
pid └─┘ └┘ └┘ └┘ └┘ └─┘ ┴ ┴
st └─────────┘└────────────────────────────────────────────────────────────────────┘└─────┘
898
899 variables {F} {G : J ⥤ C} (α : F ⟶ G)
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
900
901 @[simp, reassoc] lemma colim.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j :=
id ┴ └───────┘ ┴ ┴ ┴ └───┘└──┘ ┴ ┴ ┴└──┘ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ ┴ └───┘└──┘ ┴ └──┘ ┴ └───────┘
typ ┴ └───────┘ ┴ ┴ ┴ └───┘└──┘ ┴ ┴ ┴└──┘ ┴ ┴ └───────┘ ┴ ┴
doc └──┘ └─────┘ └───┘
902 by apply is_colimit.fac
id └────────────┘
src └────┘ └
typ └────┘└────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st └─────────────────────
903
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
904 @[simp] lemma colimit.map_desc (c : cocone G) :
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └──┘ └────┘
905 colim.map α ≫ colimit.desc G c = colimit.desc F ((cocones.precompose α).obj c) :=
id └───┘└──┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ └────────────────┘ ┴ └─┘ ┴
src └───┘└──┘ ┴ └──────────┘ ┴ └──────────┘ └────────────────┘ └─┘
typ └───┘└──┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ └────────────────┘ ┴ └─┘ ┴
doc └───┘
906 by ext; rw [←assoc, colim.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]; refl
id └───┘ └─────────┘ └───┘ └────────────┘ └────────────┘
src └─┘ └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘└┘└────────────┘┴ └────
typ └─┘ └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘└┘└────────────┘┴ └────
doc └─┘ └───┘ └┘ └┘ └┘└────────────┘└┘└────────────┘┴ └────
txt └─┘ └───┘ └┘ └┘ └┘ └┘ ┴ └────
par └─┘ └───┘ └┘ └┘ └┘ └┘ ┴ └────
pid └─┘ └┘ └┘ └┘ └┘ ┴ └
st └────────┘└────┘└───────────┘└─────┘└──────────────┘└──────────────┘┴└──────
907
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
908 lemma colimit.pre_map [has_colimits_of_shape K C] (E : K ⥤ J) :
id └───────────────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────────┘ ┴
909 colimit.pre F E ≫ colim.map α = colim.map (whisker_left E α) ≫ colimit.pre G E :=
id └─────────┘ ┴ ┴ ┴ └───┘└──┘ ┴ ┴ └───┘└──┘ └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └─────────┘ ┴ └───┘└──┘ ┴ └───┘└──┘ └──────────┘ ┴ └─────────┘
typ └─────────┘ ┴ ┴ ┴ └───┘└──┘ ┴ ┴ └───┘└──┘ └──────────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └───┘ └───┘
910 by ext; rw [←assoc, colimit.ι_pre, colim.ι_map, ←assoc, colim.ι_map, assoc, colimit.ι_pre]; refl
id └───┘ └───────────┘ └─────────┘ └───┘ └─────────┘ └───┘ └───────────┘
src └─┘ └───┘└───┘└┘└───────────┘└┘└─────────┘└─┘└───┘└┘└─────────┘└┘└───┘└┘└───────────┘┴ └────
typ └─┘ └───┘└───┘└┘└───────────┘└┘└─────────┘└─┘└───┘└┘└─────────┘└┘└───┘└┘└───────────┘┴ └────
doc └─┘ └───┘ └┘ └┘ └─┘ └┘ └┘ └┘ ┴ └────
txt └─┘ └───┘ └┘ └┘ └─┘ └┘ └┘ └┘ ┴ └────
par └─┘ └───┘ └┘ └┘ └─┘ └┘ └┘ └┘ ┴ └────
pid └─┘ └┘ └┘ └─┘ └┘ └┘ └┘ ┴ └
st └────────┘└────┘└─────────────┘└───────────┘└──────┘└───────────┘└─────┘└─────────────┘┴└──────
911
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
912 lemma colimit.pre_map' [has_colimits_of_shape.{v} K C]
id └───────────────────┘ ┴ ┴
src └───────────────────┘
typ └───────────────────┘ ┴ ┴
doc └───────────────────┘
913 (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘
doc ┴ ┴
914 colimit.pre F E₁ = colim.map (whisker_right α F) ≫ colimit.pre F E₂ :=
id └─────────┘ ┴ └┘ ┴ └───┘└──┘ └───────────┘ ┴ ┴ ┴ └─────────┘ ┴ └┘
src └─────────┘ ┴ └───┘└──┘ └───────────┘ ┴ └─────────┘
typ └─────────┘ ┴ └┘ ┴ └───┘└──┘ └───────────┘ ┴ ┴ ┴ └─────────┘ ┴ └┘
doc └───┘
915 by ext1; simp [(category.assoc _ _ _ _).symm]
id └────────────┘
src └──┘ └────┘ └────────────┘└───────────────
typ └──┘ └────┘ └────────────┘└───────────────
doc └──┘ └────┘ └───────────────
txt └──┘ └────┘ └───────────────
par └──┘ └────┘ └───────────────
pid ┴┴ └─────────────┘└
st └───────────────────────────────────────────
916
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
917 lemma colimit.pre_id (F : J ⥤ C) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
doc ┴
918 colimit.pre F (𝟭 _) = colim.map (functor.left_unitor F).hom := by tidy
id └─────────┘ ┴ ┴ ┴ └───┘└──┘ └─────────────────┘ ┴ └─┘
src └─────────┘ ┴ ┴ └───┘└──┘ └─────────────────┘ └─┘ └────
typ └─────────┘ ┴ ┴ ┴ └───┘└──┘ └─────────────────┘ ┴ └─┘ └────
doc ┴ └───┘ └────
txt └────
par └────
pid └
st └─────
919
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
920 lemma colimit.map_post {D : Type u'} [category.{v} D] [has_colimits_of_shape J D] (H : C ⥤ D) :
id └──────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ └───────────────────┘ ┴
typ └──────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └───────────────────┘ ┴
921 /- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
922 H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/
923 colimit.post F H ≫ H.map (colim.map α) = colim.map (whisker_right α H) ≫ colimit.post G H:=
id └──────────┘ ┴ ┴ ┴ ┴└──┘ └───┘└──┘ ┴ ┴ └───┘└──┘ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ ┴ └──┘ └───┘└──┘ ┴ └───┘└──┘ └───────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴└──┘ └───┘└──┘ ┴ ┴ └───┘└──┘ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
doc └───┘ └───┘
924 begin
st └─────
925 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
926 rw [←assoc, colimit.ι_post, ←H.map_comp, colim.ι_map, H.map_comp],
id └───┘ └────────────┘ └─────────┘
src └───┘└───┘└┘└────────────┘└─┘ └┘└─────────┘└┘ ┴
typ └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└─────────┘└┘└────────┘┴
doc └───┘ └┘ └─┘ └┘ └┘ ┴
txt └───┘ └┘ └─┘ └┘ └┘ ┴
par └───┘ └┘ └─┘ └┘ └┘ ┴
pid └─┘ └┘ └─┘ └┘ └┘ ┴
st ───────────┘└──────────────┘└───────────┘└───────────┘└──────────┘└──
927 rw [←assoc, colim.ι_map, assoc, colimit.ι_post],
id └───┘ └─────────┘ └───┘ └────────────┘
src └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘┴
typ └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘┴
doc └───┘ └┘ └┘ └┘ ┴
txt └───┘ └┘ └┘ └┘ ┴
par └───┘ └┘ └┘ └┘ ┴
pid └─┘ └┘ └┘ └┘ ┴
st ───────────┘└───────────┘└─────┘└──────────────┘└──
928 refl
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
929 end
st └─┘
930
931 def colim_coyoneda : colim.op ⋙ coyoneda ≅ category_theory.cocones J C :=
id └───┘└─┘ ┴ └──────┘ ┴ └─────────────────────┘ ┴ ┴
src └───┘└─┘ ┴ └──────┘ ┴ └─────────────────────┘
typ └───┘└─┘ ┴ └──────┘ ┴ └─────────────────────┘ ┴ ┴
doc └───┘ ┴ └─────────────────────┘
932 nat_iso.of_components (λ F, nat_iso.of_components (colimit.hom_iso (unop F)) (by tidy))
id └───────────────────┘ ┴ └───────────────────┘ └─────────────┘ └──┘ ┴
src └───────────────────┘ └───────────────────┘ └─────────────┘ └──┘ └──┘
typ └───────────────────┘ ┴ └───────────────────┘ └─────────────┘ └──┘ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
933 (by tidy)
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
934
935 end colim_functor
936
937 def has_colimits_of_shape_of_equivalence {J' : Type v} [small_category J']
id └────────────┘ └┘
src └────────────┘
typ └────────────┘ └┘
doc └────────────┘
938 (e : J ≌ J') [has_colimits_of_shape J C] : has_colimits_of_shape J' C :=
id ┴ ┴ └┘ └───────────────────┘ ┴ ┴ └───────────────────┘ └┘ ┴
src ┴ └───────────────────┘ └───────────────────┘
typ ┴ ┴ └┘ └───────────────────┘ ┴ ┴ └───────────────────┘ └┘ ┴
doc ┴ └───────────────────┘ └───────────────────┘
939 by { constructor, intro F, apply has_colimit_of_equivalence_comp e, apply_instance }
id └─────────────────────────────┘ ┴
src └─────────┘ └─────┘ └────┘└─────────────────────────────┘┴ └─────────────┘
typ └─────────┘ └─────┘ └────┘└─────────────────────────────┘┴┴ └─────────────┘
doc └─────────┘ └─────┘ └────┘ ┴ └─────────────┘
txt └─────────┘ └─────┘ └────┘ ┴ └─────────────┘
par └─────────┘ └─────┘ └────┘ ┴ └─────────────┘
pid └┘ ┴ ┴ ┴
st └────────────┘└───────┘└───────────────────────────────────────┘└───────────────┘└┘
940
941 end colimit
942
943 end category_theory.limits